FOM: Cantor'sTheorem & Paradoxes & Continuum Hypothesis

[Andrej Bauer]

"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
> observations about the logical?
> 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
> a padagogical point about the _virtu_ of constructive
> 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