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

[Andrej Bauer]

Arnon Avron wrote:
> 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?

Oops, I intended to send this question only to Arnon personally.

It is one thing to see whether the meta-mathematics of 
intuitionistic/constructive mathematics is classical as done in 
practice, and another to what extent, if any, it must be classical. (But 
I agree we do not need a discussion in this direction just now, as we 
would not want to stifle the discussion on the Lucas-Penrose thesis.)

You have already mentioned some examples which show that the practice is 
often classical. I myself would add to this the fact that more topos 
theory is classical than seems strictly necessary, and that it is not in 
the tradition of constructive mathematics to use meta-mathematical tools.

Andrej