src/ZF/Constructible/README.html
author wenzelm
Thu Sep 02 00:48:07 2010 +0200 (2010-09-02)
changeset 38980 af73cf0dc31f
parent 36862 952b2b102a0a
permissions -rw-r--r--
turned show_question_marks into proper configuration option;
show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;
tuned;
     1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     2 
     3 <html>
     4 
     5 <head>
     6   <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
     7   <title>ZF/Constructible/README</title>
     8 </head>
     9 
    10 <body>
    11 <h1>Constructible--Relative Consistency of the Axiom of Choice</h1>
    12 
    13 G&ouml;del's proof of the relative consistency of the axiom of choice is
    14 mechanized using Isabelle/ZF.  The proof builds upon a previous mechanization
    15 of the
    16 <a href="http://www.cl.cam.ac.uk/users/lcp/papers/Sets/reflection.pdf">reflection
    17 theorem</a>.  The heavy reliance on metatheory in the original proof makes the
    18 formalization unusually long, and not entirely satisfactory: two parts of the
    19 proof do not fit together.  It seems impossible to solve these problems
    20 without formalizing the metatheory.  However, the present development follows
    21 a standard textbook, Kunen's <strong>Set Theory</strong>, and could support the
    22 formalization of further material from that book.  It also serves as an
    23 example of what to expect when deep mathematics is formalized.  
    24 
    25 A paper describing this development is
    26 <a href="http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-551.pdf">available</a>.
    27 
    28 <hr>
    29 
    30 <p>
    31 
    32 Last modified $Date$
    33 
    34 <address>
    35 <a href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>,
    36 <a href="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</a>
    37 </address>
    38 </body>
    39 </html>