[FOM] Excluded middle & cardinality of the reals

[Matthew Frank]

In response to Keith Johnson's questions:

> (a) What is IZF?

IZF = intuitionist Zermelo-Frankel set theory.  A good source on it is 
Michael Beeson's book on Foundations Of Constructive Mathematics.

> (b) how is it possible to prove that the reals are not in 1-1
> correspondence with the integers but for there to be an injection--
> and, hence, a bijection--from the reals to the natural numbers?

The problem is that you can't go constructively from the injection to the
bijection.

Example:  Let S be the set of Godel-numbers of the non-theorems of Peano
arithmetic.  Then, clearly, S is infinite and there is an injection from
S to the natural numbers.  However, we can not constructively prove that
there is a bijection between S and the natural numbers:  a constructive
proof would give a recursive bijection, contradicting the fact that S is
not recursively enumerable.

--Matt