[FOM] Gödel on intuitionism and LEM

Vladimir Sazonov V.Sazonov at csc.liv.ac.uk
Thu Oct 13 18:00:06 EDT 2005

Quoting Martin Davis <martin at eipye.com>:

> See his essay in vol. III of his Collected Works, pp. 189-201.
> He remarks that although excluded middle doesn't hold for intuitionistic 
> disjunction, it does hold intuitionistically if (p v q) is DEFINED in terms 
> of intuitionistic negation and conjunction as
> ~(~p & ~q).

There is a related point of view according to which neither 
classical logic is "useless" nor intuitionistic logic is a 
restriction of classical: 

Intuitionistic logic is nothing else as extension of classical 
logic by new intuitionistic connectives.  (I do not know who 
first suggested this.) Thus, classical connectives should rather 
be considered as primitives alongside with intuitionistic connectives. 

>From my (neutral) formalist point of view, there are various 
kinds of mathematical intuitions and supporting them formalisms. 
None of them could pretend to be the only one correct. 
All of them together constitute mathematics. 

Vladimir Sazonov

This message was sent using IMP, the Internet Messaging Program.

More information about the FOM mailing list