[FOM] NBG, Subsets and Cantor's Theorem
T.Forster@dpmms.cam.ac.uk
T.Forster at dpmms.cam.ac.uk
Tue Apr 10 12:53:26 EDT 2007
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
>
More information about the FOM
mailing list