[FOM] Excluded middle & cardinality of the reals

[Matthew Frank]

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