documents for ZF-AC and ZF-Constructible
authorpaulson
Thu Jul 29 12:15:53 2004 +0200 (2004-07-29)
changeset 15083a471fd1d9961
parent 15082 6c3276a2735b
child 15084 07f7b158ef32
documents for ZF-AC and ZF-Constructible
src/ZF/AC/document/root.bib
src/ZF/AC/document/root.tex
src/ZF/Constructible/document/root.bib
src/ZF/Constructible/document/root.tex
src/ZF/IsaMakefile
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/ZF/AC/document/root.bib	Thu Jul 29 12:15:53 2004 +0200
     1.3 @@ -0,0 +1,15 @@
     1.4 +@ARTICLE{paulson-gr,
     1.5 +  author = {Lawrence C. Paulson and Krzysztof Gr\c{a}bczewski},
     1.6 +  title = {Mechanizing Set Theory: Cardinal Arithmetic and the Axiom of Choice},
     1.7 +  journal = {Journal of Automated Reasoning},
     1.8 +  year = {1996},
     1.9 +  volume = {17},
    1.10 +  number = {3},
    1.11 +  pages = {291-323},
    1.12 +  month = dec}
    1.13 +
    1.14 +@Book{rubin&rubin,
    1.15 +  author	= {Herman Rubin and Jean E. Rubin},
    1.16 +  title		= {Equivalents of the Axiom of Choice, {II}},
    1.17 +  publisher	= "North-Holland",
    1.18 +  year		= 1985}
     2.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.2 +++ b/src/ZF/AC/document/root.tex	Thu Jul 29 12:15:53 2004 +0200
     2.3 @@ -0,0 +1,41 @@
     2.4 +\documentclass[11pt,a4paper]{article}
     2.5 +\usepackage{graphicx}
     2.6 +\usepackage{isabelle,amssymb,isabellesym}
     2.7 +\usepackage{pdfsetup}\urlstyle{rm}
     2.8 +
     2.9 +%table of contents is too crowded!
    2.10 +\usepackage{tocloft}
    2.11 +\addtolength\cftsubsecnumwidth {0.5em}
    2.12 +\addtolength\cftsubsubsecnumwidth {1.0em}
    2.13 +
    2.14 +\begin{document}
    2.15 +
    2.16 +\title{Equivalents of the Axiom of Choice}
    2.17 +\author{Krzysztof Gr\c{a}bczewski}
    2.18 +\maketitle
    2.19 +
    2.20 +\begin{abstract}
    2.21 +  This development~\cite{paulson-gr} proves the equivalence of seven
    2.22 +  formulations of the well-ordering theorem and twenty formulations of the
    2.23 +  axiom of choice. It formalizes the first two chapters of the monograph
    2.24 +  \emph{Equivalents of the Axiom of Choice} by Rubin and
    2.25 +  Rubin~\cite{rubin&rubin}. Some of this mmaterial involves extremely complex
    2.26 +  techniques.
    2.27 +\end{abstract}
    2.28 +
    2.29 +\tableofcontents
    2.30 +
    2.31 +\begin{center}
    2.32 +  \includegraphics[scale=0.7]{session_graph}
    2.33 +\end{center}
    2.34 +
    2.35 +\newpage
    2.36 +
    2.37 +\parindent 0pt\parskip 0.5ex
    2.38 +
    2.39 +\input{session}
    2.40 +
    2.41 +\bibliographystyle{plain}
    2.42 +\bibliography{root}
    2.43 +
    2.44 +\end{document}
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/ZF/Constructible/document/root.bib	Thu Jul 29 12:15:53 2004 +0200
     3.3 @@ -0,0 +1,40 @@
     3.4 +@incollection{goedel40,
     3.5 +  author	= {Kurt G\"odel},
     3.6 +  title		= {The Consistency of the Axiom of Choice and of the
     3.7 +		   Generalized Continuum Hypothesis with the Axioms of Set
     3.8 +		   Theory},
     3.9 +  booktitle	= {{Kurt G\"odel}: Collected Works},
    3.10 +  volume	= {II},
    3.11 +  editor	= {S. Feferman and others},
    3.12 +  publisher	= {Oxford University Press},
    3.13 +  year		= 1990},
    3.14 +  pages		= {33-101},
    3.15 +  note		= {First published in 1940 by Princeton University Press}}
    3.16 +
    3.17 +@Book{kunen80,
    3.18 +  author	= {Kenneth Kunen},
    3.19 +  title		= {Set Theory: An Introduction to Independence Proofs},
    3.20 +  publisher	= "North-Holland",
    3.21 +  year		= 1980}
    3.22 +
    3.23 +@ARTICLE{paulson-consistency,
    3.24 +  author = {Lawrence C. Paulson},
    3.25 +  title = {The Relative Consistency of the Axiom of Choice --- Mechanized Using {Isabelle/ZF}},
    3.26 +  journal = {LMS Journal of Computation and Mathematics},
    3.27 +  year = {2003},
    3.28 +  volume = {6},
    3.29 +  pages = {198-248},
    3.30 +  note = {\url{http://www.lms.ac.uk/jcm/6/lms2003-001/}},
    3.31 +}
    3.32 +
    3.33 +@INPROCEEDINGS{paulson-reflection,
    3.34 +  author = {Lawrence C. Paulson},
    3.35 +  title = {The Reflection Theorem: A Study in Meta-Theoretic Reasoning},
    3.36 +  pages = {377-391},
    3.37 +  editor	= {Andrei Voronkov},
    3.38 +  booktitle	= {Automated Deduction --- {CADE}-18 
    3.39 +		  International Conference},
    3.40 +  year		= 2002,
    3.41 +  series	= {LNAI 2392},
    3.42 +  publisher	= {Springer}}
    3.43 +}
     4.1 --- a/src/ZF/Constructible/document/root.tex	Wed Jul 28 16:26:27 2004 +0200
     4.2 +++ b/src/ZF/Constructible/document/root.tex	Thu Jul 29 12:15:53 2004 +0200
     4.3 @@ -3,17 +3,41 @@
     4.4  \usepackage{isabelle,amssymb,isabellesym}
     4.5  \usepackage{pdfsetup}\urlstyle{rm}
     4.6  
     4.7 -%table of contents too crowded!
     4.8 +%table of contents is too crowded!
     4.9  \usepackage{tocloft}
    4.10  \addtolength\cftsubsecnumwidth {0.5em}
    4.11  \addtolength\cftsubsubsecnumwidth {1.0em}
    4.12  
    4.13  \begin{document}
    4.14  
    4.15 -\title{Constructible}
    4.16 +\title{The Constructible Universe\\ and the\\
    4.17 +       Relative Consistency of the Axiom of Choice}
    4.18  \author{Lawrence C Paulson}
    4.19  \maketitle
    4.20  
    4.21 +\begin{abstract}
    4.22 +  G\"odel's proof of the relative consistency of the axiom of
    4.23 +  choice~\cite{goedel40} is one of the most important results in the
    4.24 +  foundations of mathematics. It bears on Hilbert's first problem, namely the
    4.25 +  continuum hypothesis, and indeed G\"odel also proved the relative
    4.26 +  consistency of the continuum hypothesis. Just as important, G\"odel's proof
    4.27 +  introduced the \emph{inner model} method of proving relative consistency,
    4.28 +  and it introduced the concept of \emph{constructible
    4.29 +    set}. Kunen~\cite{kunen80} gives an excellent description of this body of
    4.30 +  work.
    4.31 +  
    4.32 +  This Isabelle/ZF formalization demonstrates G\"odel's claim that his proof
    4.33 +  can be undertaken without using metamathematical arguments, for example
    4.34 +  arguments based on the general syntactic structure of a formula. Isabelle's
    4.35 +  automation replaces the metamathematics, although it does not eliminate the
    4.36 +  requirement at least to state many tedious results that would otherwise be
    4.37 +  unnecessary.
    4.38 +  
    4.39 +  This formalization~\cite{paulson-consistency} is by far the deepest result
    4.40 +  in set theory proved in any automated theorem prover. It rests on a previous
    4.41 +  formal development of the reflection theorem~\cite{paulson-reflection}.
    4.42 +\end{abstract}
    4.43 +
    4.44  \tableofcontents
    4.45  
    4.46  \begin{center}
    4.47 @@ -26,7 +50,7 @@
    4.48  
    4.49  \input{session}
    4.50  
    4.51 -%\bibliographystyle{abbrv}
    4.52 -%\bibliography{root}
    4.53 +\bibliographystyle{plain}
    4.54 +\bibliography{root}
    4.55  
    4.56  \end{document}
     5.1 --- a/src/ZF/IsaMakefile	Wed Jul 28 16:26:27 2004 +0200
     5.2 +++ b/src/ZF/IsaMakefile	Thu Jul 29 12:15:53 2004 +0200
     5.3 @@ -59,8 +59,8 @@
     5.4    AC/AC16_lemmas.thy AC/AC17_AC1.thy AC/AC18_AC19.thy AC/AC7_AC9.thy \
     5.5    AC/AC_Equiv.thy AC/Cardinal_aux.thy \
     5.6    AC/DC.thy AC/HH.thy AC/Hartog.thy AC/WO1_AC.thy AC/WO1_WO7.thy \
     5.7 -  AC/WO2_AC16.thy AC/WO6_WO1.thy 
     5.8 -	@$(ISATOOL) usedir $(OUT)/ZF AC
     5.9 +  AC/WO2_AC16.thy AC/WO6_WO1.thy AC/document/root.bib AC/document/root.tex
    5.10 +	@$(ISATOOL) usedir -g true $(OUT)/ZF AC
    5.11  
    5.12  
    5.13  ## ZF-Coind
    5.14 @@ -87,7 +87,7 @@
    5.15    Constructible/Rec_Separation.thy Constructible/Separation.thy \
    5.16    Constructible/Satisfies_absolute.thy Constructible/WF_absolute.thy \
    5.17    Constructible/Reflection.thy  Constructible/WFrec.thy \
    5.18 -  Constructible/document/root.tex
    5.19 +  Constructible/document/root.bib Constructible/document/root.tex
    5.20  	@$(ISATOOL) usedir -g true $(OUT)/ZF Constructible
    5.21  
    5.22