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