--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/document/root.bib Thu Jul 29 12:15:53 2004 +0200
@@ -0,0 +1,15 @@
+@ARTICLE{paulson-gr,
+ author = {Lawrence C. Paulson and Krzysztof Gr\c{a}bczewski},
+ title = {Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice},
+ journal = {Journal of Automated Reasoning},
+ year = {1996},
+ volume = {17},
+ number = {3},
+ pages = {291-323},
+ month = dec}
+
+@Book{rubin&rubin,
+ author = {Herman Rubin and Jean E. Rubin},
+ title = {Equivalents of the Axiom of Choice, {II}},
+ publisher = "North-Holland",
+ year = 1985}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/AC/document/root.tex Thu Jul 29 12:15:53 2004 +0200
@@ -0,0 +1,41 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage{graphicx}
+\usepackage{isabelle,amssymb,isabellesym}
+\usepackage{pdfsetup}\urlstyle{rm}
+
+%table of contents is too crowded!
+\usepackage{tocloft}
+\addtolength\cftsubsecnumwidth {0.5em}
+\addtolength\cftsubsubsecnumwidth {1.0em}
+
+\begin{document}
+
+\title{Equivalents of the Axiom of Choice}
+\author{Krzysztof Gr\c{a}bczewski}
+\maketitle
+
+\begin{abstract}
+ This development~\cite{paulson-gr} proves the equivalence of seven
+ formulations of the well-ordering theorem and twenty formulations of the
+ axiom of choice. It formalizes the first two chapters of the monograph
+ \emph{Equivalents of the Axiom of Choice} by Rubin and
+ Rubin~\cite{rubin&rubin}. Some of this mmaterial involves extremely complex
+ techniques.
+\end{abstract}
+
+\tableofcontents
+
+\begin{center}
+ \includegraphics[scale=0.7]{session_graph}
+\end{center}
+
+\newpage
+
+\parindent 0pt\parskip 0.5ex
+
+\input{session}
+
+\bibliographystyle{plain}
+\bibliography{root}
+
+\end{document}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/ZF/Constructible/document/root.bib Thu Jul 29 12:15:53 2004 +0200
@@ -0,0 +1,40 @@
+@incollection{goedel40,
+ author = {Kurt G\"odel},
+ title = {The Consistency of the Axiom of Choice and of the
+ Generalized Continuum Hypothesis with the Axioms of Set
+ Theory},
+ booktitle = {{Kurt G\"odel}: Collected Works},
+ volume = {II},
+ editor = {S. Feferman and others},
+ publisher = {Oxford University Press},
+ year = 1990},
+ pages = {33-101},
+ note = {First published in 1940 by Princeton University Press}}
+
+@Book{kunen80,
+ author = {Kenneth Kunen},
+ title = {Set Theory: An Introduction to Independence Proofs},
+ publisher = "North-Holland",
+ year = 1980}
+
+@ARTICLE{paulson-consistency,
+ author = {Lawrence C. Paulson},
+ title = {The Relative Consistency of the Axiom of Choice --- Mechanized Using {Isabelle/ZF}},
+ journal = {LMS Journal of Computation and Mathematics},
+ year = {2003},
+ volume = {6},
+ pages = {198-248},
+ note = {\url{http://www.lms.ac.uk/jcm/6/lms2003-001/}},
+}
+
+@INPROCEEDINGS{paulson-reflection,
+ author = {Lawrence C. Paulson},
+ title = {The Reflection Theorem: A Study in Meta-Theoretic Reasoning},
+ pages = {377-391},
+ editor = {Andrei Voronkov},
+ booktitle = {Automated Deduction --- {CADE}-18
+ International Conference},
+ year = 2002,
+ series = {LNAI 2392},
+ publisher = {Springer}}
+}
--- a/src/ZF/Constructible/document/root.tex Wed Jul 28 16:26:27 2004 +0200
+++ b/src/ZF/Constructible/document/root.tex Thu Jul 29 12:15:53 2004 +0200
@@ -3,17 +3,41 @@
\usepackage{isabelle,amssymb,isabellesym}
\usepackage{pdfsetup}\urlstyle{rm}
-%table of contents too crowded!
+%table of contents is too crowded!
\usepackage{tocloft}
\addtolength\cftsubsecnumwidth {0.5em}
\addtolength\cftsubsubsecnumwidth {1.0em}
\begin{document}
-\title{Constructible}
+\title{The Constructible Universe\\ and the\\
+ Relative Consistency of the Axiom of Choice}
\author{Lawrence C Paulson}
\maketitle
+\begin{abstract}
+ G\"odel's proof of the relative consistency of the axiom of
+ choice~\cite{goedel40} is one of the most important results in the
+ foundations of mathematics. It bears on Hilbert's first problem, namely the
+ continuum hypothesis, and indeed G\"odel also proved the relative
+ consistency of the continuum hypothesis. Just as important, G\"odel's proof
+ introduced the \emph{inner model} method of proving relative consistency,
+ and it introduced the concept of \emph{constructible
+ set}. Kunen~\cite{kunen80} gives an excellent description of this body of
+ work.
+
+ This Isabelle/ZF formalization demonstrates G\"odel's claim that his proof
+ can be undertaken without using metamathematical arguments, for example
+ arguments based on the general syntactic structure of a formula. Isabelle's
+ automation replaces the metamathematics, although it does not eliminate the
+ requirement at least to state many tedious results that would otherwise be
+ unnecessary.
+
+ This formalization~\cite{paulson-consistency} is by far the deepest result
+ in set theory proved in any automated theorem prover. It rests on a previous
+ formal development of the reflection theorem~\cite{paulson-reflection}.
+\end{abstract}
+
\tableofcontents
\begin{center}
@@ -26,7 +50,7 @@
\input{session}
-%\bibliographystyle{abbrv}
-%\bibliography{root}
+\bibliographystyle{plain}
+\bibliography{root}
\end{document}
--- a/src/ZF/IsaMakefile Wed Jul 28 16:26:27 2004 +0200
+++ b/src/ZF/IsaMakefile Thu Jul 29 12:15:53 2004 +0200
@@ -59,8 +59,8 @@
AC/AC16_lemmas.thy AC/AC17_AC1.thy AC/AC18_AC19.thy AC/AC7_AC9.thy \
AC/AC_Equiv.thy AC/Cardinal_aux.thy \
AC/DC.thy AC/HH.thy AC/Hartog.thy AC/WO1_AC.thy AC/WO1_WO7.thy \
- AC/WO2_AC16.thy AC/WO6_WO1.thy
- @$(ISATOOL) usedir $(OUT)/ZF AC
+ AC/WO2_AC16.thy AC/WO6_WO1.thy AC/document/root.bib AC/document/root.tex
+ @$(ISATOOL) usedir -g true $(OUT)/ZF AC
## ZF-Coind
@@ -87,7 +87,7 @@
Constructible/Rec_Separation.thy Constructible/Separation.thy \
Constructible/Satisfies_absolute.thy Constructible/WF_absolute.thy \
Constructible/Reflection.thy Constructible/WFrec.thy \
- Constructible/document/root.tex
+ Constructible/document/root.bib Constructible/document/root.tex
@$(ISATOOL) usedir -g true $(OUT)/ZF Constructible