[FOM] The uncountability of continuum. 1.

[Hendrik Boom]

On Tue, Mar 08, 2005 at 01:22:37AM +0300, Alexander Zenkin wrote:
> 
> 	Some FOMers were uttering an opinion that there are two different
> proofs of the uncountability of continuum: 
> 	1) the direct proof given by Cantor in 1873/4 and
> 	2) the indirect proof (by Reductio ad Absurdum (RAA)) given by
> Cantor in 1890/1 
> (as a special case of the common proof of the inequality |P(Z)| > |Z| for
> any set Z).

Let me look at this constructively.

The operative part of any of these proofs is the subproof that, given any
enumeration of real numbers, there is a real number not enumerated.  This
can be done constructively.

Whether there is a constructive proof of the uncountability of reals
may depend on just how you define uncountability.  If you define it
by saying something like, "NOT (there is a one-to-one correspondence ...)"
uncountability is a negative statement.  Now (NOT P) means (P implies FALSE).
A proof of P implies FALSE is a Reductio ad Absurdum (or contains one somewhere
within it).

So constructively, a direct proof of the uncountability of the continuum
is a reduction ad absurdum.

Is there another way to define uncountability?  Perhaps by defining it as
"Every countable enumeration leaves something out."  If you do that,
there is an obvious direct proof.


-- hendrik