[FOM] NBG, Subsets and Cantor's Theorem

[T.Forster@dpmms.cam.ac.uk]

It is of course possible to paint a picture of this subject matter in such 
a way as to conceal the role of the axiom scheme of separation, the better 
to emphasise other aspects, and Andrej has done this. However the fact 
remains that separation *is* necessary. Cantor's theorem fails in Church's 
set theory and in NFU, where separation is restricted. And famously, 
cartesian-closedness of the topos of sets needs some separation as well.


On Apr 9 2007, Andrej Bauer wrote:

>There is a proof following an idea of Lawvere of Cantor's theorem which 
>only uses bounded separation to first establish a general fact about set 
>theory, namely that sets form a cartesian closed category. The other bit 
>of knowledge that is needed is that the powerset P(A) is isomorphic to 
>the exponential Omega^A, where Omega is the set of truth values. Details 
>of the proof are explained at
>
>http://math.andrej.com/2007/04/08/on-a-proof-of-cantors-theorem/
>
>for those who are interested. Thus, if one axiomatizes set theory so 
>that the cartesian closed structure is explicit (as is usually done in 
>e.g. topos theory) rather than derived from powersets via bounded 
>separation, then Cantor's theorem becomes a simple lambda-calculus 
>calculation. I would therefore say that the axiom of separation is not 
>an essential ingridient of Cantor's theorem.
>
>Best regards,
>
>Andrej
>
>_______________________________________________
>FOM mailing list
>FOM at cs.nyu.edu
>http://www.cs.nyu.edu/mailman/listinfo/fom
>