[FOM] Excluded middle & cardinality of the reals
Matthew Frank
mfrank at math.uchicago.edu
Sat Jul 3 19:40:54 EDT 2004
I cited Charles McCarty as claiming that:
> > However, it is compatible with constructive math (or at least, compatible
> > with IZF) that every set has an injection into the natural numbers. See
This is not quite correct. However, McCarty did prove that:
It is consistent with IZF that every set with an apartness relation is the
image of some function whose domain is a subset of the natural numbers.
Here, an apartness relation is a relation # on a set x such that
forall y and z in x:
y = z -> not y#z
y#z <-> z#y
y#z -> (forall r in x)(y#r or z#r)
In particular, the reals have the apartness relation |x-y|>0.
I think Jaap Voosten for pointing out my error, and for pointing me to
the correct statement. --Matt
More information about the FOM
mailing list