FOM: Cantor's Theorem & Paradoxes & Continuum Hypothesis

[William Tait]

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