[FOM] An intuitionistic query

[Thomas Lord]

On Fri, 2009-09-11 at 21:41 +0100, Thomas Forster wrote:
> > For any of these interpretations, I have a related question.
> > Is the following intuitive implication
> >     A={a,b,c}  ==>   |A|=1 v |A|=2 v |A|=3      (**)
> > intuitionistically valid?
> > 
>     No, because it implies that all equations between a,b and c obey 
> excluded middle.

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?


-t