[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?
Robert
More information about the FOM
mailing list