# FOM: Cantor'sTheorem & Paradoxes & Continuum Hypothesis

Andrej Bauer Andrej.Bauer at andrej.com
Sun Feb 11 16:31:37 EST 2001

"Robert Tragesser" <rtragesser at hotmail.com> writes:
> Isn't it fair to say that that proof of
> Cantor's Theorem is a capital example of
> the sort of purely logical, nonconstructive
> proof which motivated Brouwer's churlish
> Is it right to say that a constructive proof
> of Cantor's Theorem would provide an answer to
> the truth of the Generalized Continuum Hypothesis?
> (I mean of course a constructive proof within
> Cantor-Zermelo set theories.)
> A "yes" here would be good for making dramatically
> proofs.

I am confused by this because Cantor's proof that there is no
surjection from a set A to its powerset is already constructive, in
the sense that it is valid in any topos. Just to be absolutely sure:

Theorem: There does not exist a surjection s: A --> P(A).

Proof: Suppose there were such a surjection s. Let U be the subset of
A defined by

U = {x \in A | not (x \in s(x))}

Because s is surjective there exists y in A such that U = s y. If
y \in U then by definition of U, not (y \in s y = U), a contradiction.
Therefore, not (y \in U). But now again by definition of U, it
follows that y \in U. Therefore, both y \in U and not (y \in U),
a contradiction. We conclude that there is no surjection s: A --> P(A).
QED

Unless I am making a silly mistake, this proof is intuitionistic.
(I seem to recall that once I was scolded by my advisor for not
realizing that this proof was intuitionistic...)

There is the possibility that Robert Tragesser means "predicative"
when he asks for a constructive proof. But what would that even mean,
given that the theorem itself already speaks of arbitrary powersets?

Andrej Bauer

Mittag-Leffler Institute, Sweden
http://andrej.com