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