[FOM] Thomas Lord's intuitionistic query

[Andreas Blass]

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