Index of /ports/math/isabelle/work/Isabelle2005/src/ZF/Constructible

      Name                    Last modified       Size  Description


[DIR] Parent Directory        09-Aug-2008 06:10      -  
[   ] AC_in_L.thy             17-Jun-2005 07:15    15k  
[TXT] AC_in_L.thy.html        09-Aug-2008 06:10     0k  
[   ] DPow_absolute.thy       17-Jun-2005 07:15    23k  
[TXT] DPow_absolute.thy.html  09-Aug-2008 06:10     0k  
[   ] Datatype_absolute.thy   17-Jun-2005 07:15    36k  
[TXT] Datatype_absolute.th..> 09-Aug-2008 06:10     0k  
[   ] Formula.thy             17-Jun-2005 07:15    32k  
[TXT] Formula.thy.html        09-Aug-2008 06:10     0k  
[   ] Internalize.thy         17-Jun-2005 07:15    53k  
[TXT] Internalize.thy.html    09-Aug-2008 06:10     0k  
[   ] L_axioms.thy            17-Jun-2005 07:15    47k  
[TXT] L_axioms.thy.html       09-Aug-2008 06:10     0k  
[   ] MetaExists.thy          17-Jun-2005 07:15     1k  
[TXT] MetaExists.thy.html     09-Aug-2008 06:10     0k  
[   ] Normal.thy              17-Jun-2005 07:15    15k  
[TXT] Normal.thy.html         09-Aug-2008 06:10     0k  
[   ] ROOT.ML                 09-Oct-2002 02:07     1k  
[TXT] ROOT.ML.html            09-Aug-2008 06:10     0k  
[   ] Rank.thy                17-Jun-2005 07:15    35k  
[TXT] Rank.thy.html           09-Aug-2008 06:10     0k  
[   ] Rank_Separation.thy     17-Jun-2005 07:15    11k  
[TXT] Rank_Separation.thy...> 09-Aug-2008 06:10     0k  
[   ] Rec_Separation.thy      17-Jun-2005 07:15    17k  
[TXT] Rec_Separation.thy.html 09-Aug-2008 06:10     0k  
[   ] Reflection.thy          17-Jun-2005 07:15    14k  
[TXT] Reflection.thy.html     09-Aug-2008 06:10     0k  
[   ] Relative.thy            17-Jun-2005 07:15    52k  
[TXT] Relative.thy.html       09-Aug-2008 06:10     0k  
[   ] Satisfies_absolute.thy  17-Jun-2005 07:15    41k  
[TXT] Satisfies_absolute.t..> 09-Aug-2008 06:10     0k  
[   ] Separation.thy          17-Jun-2005 07:15    12k  
[TXT] Separation.thy.html     09-Aug-2008 06:10     0k  
[   ] WF_absolute.thy         17-Jun-2005 07:15    12k  
[TXT] WF_absolute.thy.html    09-Aug-2008 06:10     0k  
[   ] WFrec.thy               17-Jun-2005 07:15    13k  
[TXT] WFrec.thy.html          09-Aug-2008 06:10     0k  
[   ] Wellorderings.thy       17-Jun-2005 07:15     8k  
[TXT] Wellorderings.thy.html  09-Aug-2008 06:10     0k  
[DIR] document/               09-Aug-2008 06:10      -
ZF/Constructible/README

Constructible--Relative Consistency of the Axiom of Choice

Gödel's proof of the relative consistency of the axiom of choice is mechanized using Isabelle/ZF. The proof builds upon a previous mechanization of the reflection theorem. The heavy reliance on metatheory in the original proof makes the formalization unusually long, and not entirely satisfactory: two parts of the proof do not fit together. It seems impossible to solve these problems without formalizing the metatheory. However, the present development follows a standard textbook, Kunen's Set Theory, and could support the formalization of further material from that book. It also serves as an example of what to expect when deep mathematics is formalized. A paper describing this development is available.

Last modified $Date: 2005/03/07 18:19:12 $

Larry Paulson, lcp@cl.cam.ac.uk