[FOM] An intuitionistic query

Arnold Neumaier Arnold.Neumaier at univie.ac.at
Wed Sep 9 10:12:50 EDT 2009

```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
```