1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> |
1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd"> |
2 |
2 |
3 <HTML><HEAD><TITLE>ZF/Constructible/README</TITLE></HEAD><BODY> |
3 <!-- $Id$ --> |
4 |
4 |
5 <H1>Constructible--Relative Consistency of the Axiom of Choice</H1> |
5 <html> |
6 |
6 |
7 <P>Gödel's proof of the relative consistency of the axiom of choice is |
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ödel's proof of the relative consistency of the axiom of choice is |
8 mechanized using Isabelle/ZF. The proof builds upon a previous mechanization |
16 mechanized using Isabelle/ZF. The proof builds upon a previous mechanization |
9 of the |
17 of the |
10 <A HREF="http://www.cl.cam.ac.uk/users/lcp/papers/Sets/reflection.pdf">reflection |
18 <a href="http://www.cl.cam.ac.uk/users/lcp/papers/Sets/reflection.pdf">reflection |
11 theorem</A>. The heavy reliance on metatheory in the original proof makes the |
19 theorem</a>. The heavy reliance on metatheory in the original proof makes the |
12 formalization unusually long, and not entirely satisfactory: two parts of the |
20 formalization unusually long, and not entirely satisfactory: two parts of the |
13 proof do not fit together. It seems impossible to solve these problems |
21 proof do not fit together. It seems impossible to solve these problems |
14 without formalizing the metatheory. However, the present development follows |
22 without formalizing the metatheory. However, the present development follows |
15 a standard textbook, Kunen's <STRONG>Set Theory</STRONG>, and could support the |
23 a standard textbook, Kunen's <strong>Set Theory</strong>, and could support the |
16 formalization of further material from that book. It also serves as an |
24 formalization of further material from that book. It also serves as an |
17 example of what to expect when deep mathematics is formalized. |
25 example of what to expect when deep mathematics is formalized. |
18 |
26 |
19 A paper describing this development is |
27 A paper describing this development is |
20 <A HREF="http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-551.pdf">available</A>. |
28 <a href="http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-551.pdf">available</a>. |
21 |
29 |
22 <HR> |
30 <hr> |
23 <P>Last modified $Date$ |
|
24 |
31 |
25 <ADDRESS> |
32 <p> |
26 <A |
33 |
27 HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>, |
34 Last modified $Date$ |
28 <A HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A> |
35 |
29 </ADDRESS> |
36 <address> |
30 </BODY></HTML> |
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> |