FOM: Cantor'sTheorem & Paradoxes & Continuum Hypothesis

[Joseph Vidal-Rosset]

At 22:31 +0100 11/02/2001, Andrej Bauer wrote:
>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?

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.

Thanks for your help,
-- 
------
Joseph Vidal-Rosset
page web: http://www.u-bourgogne.fr/PHILO/joseph.vidal-rosset