[FOM] An intuitionistic query

[Arnold Neumaier]

Robert Lubarsky wrote:
> Yes. If |A|=2 then there are x and y such that, for all z in A, z=x or z=y.
> Instantiate z with each of a, b, and c. 

So you interpret |A|=n as ``there is a sequence x_k (k=1:n) of pairwise 
distinct elements such that for all z in A, z=x_k for some k=1:n''. [I1]

Frank Waaldijk and Richard heck interpreted |A|=n essentially as ``there 
is a bijection from A to the set {1,...,n}''. [I2]

[I1] and [I2] apparently define the same notion. (At least classically; 
I am not sure whether this is also the same intuitionistically - one
must apparently be extremely careful if one is not trained to think
intuitionistically.)

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?


> With an "or", one can do a case
> analysis. That is, if you have "phi or psi", you can assume first phi and
> then psi to come up with your theorem. (I.e. phi -> theta and psi -> theta
> implies (phi or psi) -> theta.) Doing this case analysis with the given
> equalities yields the desired result.

OK. This nicely proves
 >>     A={a,b,c}, |A|=2    ==>   a=b v a=c v b=c          (*)
from the definition [I1].

(*) is a special case of Dirichlet's pigeonhole principle.
Are there versions of the latter that are intuitionistically 
undecidable? I found an infinite version in
    https://eprints.kfupm.edu.sa/60600/1/60600.pdf ,
but I am looking for a finite version. Perhaps one of those in:
http://www.cs.utexas.edu/users/EWD/transcriptions/EWD09xx/EWD980.html

Also, for any of the interpretations [I1} or [I2], I have a related 
question. Is the following intuitive implication
    A={a,b,c}  ==>   |A|=1 v |A|=2 v |A|=3      (**)
intuitionistically valid?


Arnold Neumaier