[FOM] Question of the Day: What is a Logic?
Andrej.Bauer at fmf.uni-lj.si
Mon Oct 16 08:47:46 EDT 2006
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.
More information about the FOM