[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
More information about the FOM
mailing list