[FOM] An intuitionistic query

[Robert Lubarsky]

> Is the following intuitive implication
>    A={a,b,c}  ==>   |A|=1 v |A|=2 v |A|=3      (**)
> intuitionistically valid?

No. Think of a Kripke model. At the bottom node, we have the set {a,b,c}. At
three incomparable later nodes, either a, b, and c are all different, all
equal, or consist of exactly two sets. So at the starting node, you could
not assert the size is 1, 2, or 3, because one of those would then have had
to be true.