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