[FOM] Excluded middle & cardinality of the reals
mfrank at math.uchicago.edu
Sat Jun 26 12:03:39 EDT 2004
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
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.
More information about the FOM