[FOM] Intuitionism and 0=1

Robert Black Mongre at gmx.de
Thu Nov 8 04:37:55 EST 2007

In Heyting arithmetic we can define absurdity as 0=1 and then get ex 
falso sequitur quodlibet for free, since every sentence of the 
language follows from 0=1 and the axioms of HA just using minimal 
logic. (Yes, Neil, I know you don't approve of doing this, but you're 
not going to deny the formal result ...)

My question is: does this still hold once we go beyond arithmetic, in 
particular, does it hold for systems of formalized intuitionistic 
analysis? Dummett says in his book (p. 13) that it 'might not be so 
obvious', but is it true?


More information about the FOM mailing list