[FOM] Thomas Lord's intuitionistic query
Andreas Blass
ablass at umich.edu
Sat Sep 19 12:35:09 EDT 2009
Thomas Lord asked:
Is there a conventional intuitionistic object "bottom"
(as in "undecidable" or "unknowable")?
I.e., the theorem:
A = {a,b,c} ==> |A|=1 v |A|=2 v |A|=3 v |A|=\bottom
would be true?
There is no such \bottom, and for a good reason. If the theorem Lord
proposed were true, then, with A = {a,b,c} and X = {x,y,z}, it would
follow that
|A|=1 or |A|=2 or |A|=3 or |X|=1 or |X|=2 or |X|=3 or |A|=|X|
(the last clause being the case where |A| and |X| both equal
\bottom). I
can't imagine any intuitionist accepting that result.
Andreas Blass
More information about the FOM
mailing list