summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/ZF/Constructible/README.html

author | wenzelm |

Thu Sep 02 00:48:07 2010 +0200 (2010-09-02) | |

changeset 38980 | af73cf0dc31f |

parent 36862 | 952b2b102a0a |

permissions | -rw-r--r-- |

turned show_question_marks into proper configuration option;

show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;

tuned;

show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;

tuned;

1 <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">

3 <html>

5 <head>

6 <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">

7 <title>ZF/Constructible/README</title>

8 </head>

10 <body>

11 <h1>Constructible--Relative Consistency of the Axiom of Choice</h1>

13 Gödel's proof of the relative consistency of the axiom of choice is

14 mechanized using Isabelle/ZF. The proof builds upon a previous mechanization

15 of the

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

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

21 a standard textbook, Kunen's <strong>Set Theory</strong>, and could support the

22 formalization of further material from that book. It also serves as an

23 example of what to expect when deep mathematics is formalized.

25 A paper describing this development is

26 <a href="http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-551.pdf">available</a>.

28 <hr>

30 <p>

32 Last modified $Date$

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>