[FOM] uncountability of the continuum

[Randall Holmes]

Since the uncountability of the continuum is a negative statement, a
proof of this statement by contradiction is a constructive proof.
(Proof by contradiction is the standard way to prove a negative
statement constructively!)

Given any enumeration of real numbers (we do not need to make any
assumption about whether it contains all real numbers or not: this is
the mistake in Zenkin's exposition) we produce a real number which is
not in the range of that enumeration by an explicit computation (some
variant of Cantor's diagonal method).  So we have a procedure which,
given any constructive proof that the continuum can be enumerated (a
specific enumeration of reals and a constructive proof that any real
belongs to its range), would generate a contradiction.  That is what
it means to prove "the continuum cannot be enumerated" constructively.

Sincerely, Randall Holmes