<HTML><HEAD><TITLE>ZF/Constructible/README</TITLE></HEAD><BODY>
<H1>Constructible--Relative Consistency of the Axiom of Choice</H1>
<P>Gödel's proof of the relative consistency of the axiom of choice is
mechanized using Isabelle/ZF. The proof builds upon a previous mechanization
of the
<A HREF="http://www.cl.cam.ac.uk/users/lcp/papers/Sets/reflection.pdf">reflection
theorem</A>. The heavy reliance on metatheory in the original proof makes the
formalization unusually long, and not entirely satisfactory: two parts of the
proof do not fit together. It seems impossible to solve these problems
without formalizing the metatheory. However, the present development follows
a standard textbook, Kunen's <STRONG>Set Theory</STRONG>, and could support the
formalization of further material from that book. It also serves as an
example of what to expect when deep mathematics is formalized.
A paper describing this development is
<A HREF="http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-551.pdf">available</A>.
<HR>
<P>Last modified $Date$
<ADDRESS>
<A
HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>,
<A HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
</ADDRESS>
</BODY></HTML>