FOM: Cantor's Theorem & Paradoxes & Continuum Hypothesis

William Tait wwtx at midway.uchicago.edu
Mon Feb 12 19:09:06 EST 2001

Joseph Vidal-Rosset wrote (2/12/01)
>Yes, I would be happy to get how a proof based on an impredicative
>axiom can be said "constructive".
>
>The fact of the impredicativity in Cantor's theorem cannot be
>denied. Neil Tennant says rightly that in Cantor's theorem invokes
>the axiom schema of Separation, but this axiom has "the akward
>property of being impredicative" (Fraenkel, Bar-Hillel, Levy,
>Foundations of Set Theory, p. 38).
>
>It would be a happy thing for me to know how impredicativity is
>consistent with constructivity. I do not denied that it is possible,
>but I have difficulties to uderstand it.

Impredicativity, as I understand it, concerns definitions. A
definition of M is impredicative if the the definition refers to a
totality (e..g involves quantification over that totality) to which M
belongs. I don't see that Cantor's argument is impredicative. It
shows that, given a function F from a set A whose values are subsets
of A, there is a subset C of A not in the range of F.The definition
of C is: x in C iff x not in f(x). That is not an impredicative
definition.

I also see no reference in this argument to the power set P(A) of A.
P(A) gets mentioned only---and of necessity---in the conclusion that
P(A) has power greater than A. If one doesn't like power sets, then
just don't mention this result: Cantor's diagonal argument will
nevertheless stand.

As for whether impredicative definition is compatible with
constructivity, note that at least Goedel thought that his theory of
impredicative primitive recursive functions is constructive.

Best wishes from Chicago, where the sun shone today!

Bill