[FOM] Question of the Day: What is a Logic?

[Arnon Avron]

On Sun, Oct 08, 2006 at 09:34:26PM +0200, Andrej Bauer wrote:
> Dear Arnon,
> 
> why do you say that classical logic is the metalogic of 
> intuitionistic  logic?


Dear Andrej,

I shall  answer this shortly, but I prefer not to start now a 
debate on this: I am sure that declared intuitionists (*personally* I 
dont believe that there are real intuitionists, even if
some people truly believe they are) are doing their best 
to use only proof methods that are intutionistically acceptable,
but others gladly use purely classical methods in meta investigations
on intuitionism. As an example: in Takeuti's book on Proof theory
(as well as in Fitting's book on modal and intuitionist logics)
there is (if I remember correctly - I dont have the books at present)
a semantic proof of the admissibility of the cut rule
in a multiple-conclusioned Gentzen-type system for intuitionistic
logic via a proof of the completeness of the cut-free part of
that system for the Kripke semantics. As far as I remember (or can
reconstruct now  in my head) these proofs are 
not intutionistically acceptable. Perhaps they can be turned into 
ones, but I am sure that most readers are happy with the results
without bothering to check whether the proofs can so be made 
or not (oops, I am not allowed to say "whether ... or not").

  If I go deeper, I think (and you will disagree), that while
investigating intuitionist logic all of us (or at least most of us)
assume/believe that given a formal theory T, every sentence
in its language is either provable in T using LJ or not,
and that given a world w in an intuitionist Kripke frame for
a language L, every sentence of L is either forced in w or not. 
The way I see it, Kripke semantics is a classical semantics for 
intuitionist logic.

Arnon Avron