[FOM] Gödel on intuitionism and LEM

[Vladimir Sazonov]

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.