[FOM] Arnold Neumaier's question

[Neil Tennant]

In http://www.cs.nyu.edu/pipermail/fom/2009-September/014009.html, Arnold
Neumaier asks whether

A={a,b,c}, |A|=2    ==>   a=b v a=c v b=c

is intuitionistically provable.

Indeed it is.

It might be easier to see this by using the number-abstraction operator #,
instead of talking about the cardinality of a set. The question then becomes whether

#x(x=a v x=b v x=c) = ss0  intuitionistically implies (a=b v a=c v b=c).

The answer is affirmative, provided we can help ourselves to the
(innocuous) assumptions that a, b and c  exist.  That is, there is a
formal proof, in the intuitionistic logic of number, of the conclusion

	(a=b  v a=c v b=c) 

from the premises

        a exists, b exists, c exists, #x(x=a v x=b v x=c) = ss0 .

The proof is given in "A Note on Number and Identity", which can be
downloaded at

http://people.cohums.ohio-state.edu/tennant9/number_identity.pdf


Neil Tennant