[FOM] Arnold Neumaier's question
Neil Tennant
neilt at mercutio.cohums.ohio-state.edu
Tue Sep 8 21:26:03 EDT 2009
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
More information about the FOM
mailing list