|
15283
|
1 |
<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
|
|
|
2 |
|
|
15582
|
3 |
<html>
|
|
14006
|
4 |
|
|
15582
|
5 |
<head>
|
|
|
6 |
<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
|
|
|
7 |
<title>ZF/Constructible/README</title>
|
|
|
8 |
</head>
|
|
14006
|
9 |
|
|
15582
|
10 |
<body>
|
|
|
11 |
<h1>Constructible--Relative Consistency of the Axiom of Choice</h1>
|
|
|
12 |
|
|
|
13 |
Gödel's proof of the relative consistency of the axiom of choice is
|
|
14006
|
14 |
mechanized using Isabelle/ZF. The proof builds upon a previous mechanization
|
|
|
15 |
of the
|
|
15582
|
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
|
|
14006
|
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
|
|
15582
|
21 |
a standard textbook, Kunen's <strong>Set Theory</strong>, and could support the
|
|
14006
|
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
|
|
15582
|
26 |
<a href="http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-551.pdf">available</a>.
|
|
14006
|
27 |
|
|
15582
|
28 |
<hr>
|
|
|
29 |
|
|
|
30 |
<p>
|
|
14006
|
31 |
|
|
15582
|
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>
|