FOM: Cantor'sTheorem & Paradoxes & Continuum Hypothesis

[Giovanni Sambin]

Andrey Bauer writes:

>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?

A predicative statement and proof of Cantor's theorem [telling that there is no surjection from a set S into its power] is possible, and in my opinion meaningful. See theorem 2.20, page 239 of the paper:

G. Sambin - S. Valentini, Building up a toolbox for Martin-Loef's type theory: subset theory
in: G. Sambin & J. Smith eds, Twenty-five years of constructive type theory, Oxford Logic Guides 36, Oxford U.P. 1998

Of course, one has to suitably define subsets of a set S (= propositional functions with one argument in S) and functions from a set S into the collection of its subsets (= binary relations on S = propositional functions with two arguments in S). Then the proof is easy, and it is essentially the same as that recalled by Andrey Bauer.
One can find all the motivations, definitions and details in the paper mentioned above.

Giovanni Sambin
Professor of Mathematical Logic, University of Padua (Italy)
Present interests: "weak" logics, constructive mathematics (formal topology), type theory, philosophy of mathematics
www page: http://www.math.unipd.it/~sambin