[FOM] NBG, Subsets and Cantor's Theorem

[Andrej Bauer]

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