src/ZF/Constructible/document/root.tex
 author ballarin Thu Dec 11 18:30:26 2008 +0100 (2008-12-11) changeset 29223 e09c53289830 parent 15083 a471fd1d9961 permissions -rw-r--r--
Conversion of HOL-Main and ZF to new locales.
     1 \documentclass[11pt,a4paper]{article}

     2 \usepackage{graphicx}

     3 \usepackage{isabelle,amssymb,isabellesym}

     4 \usepackage{pdfsetup}\urlstyle{rm}

     5

     6 %table of contents is too crowded!

     7 \usepackage{tocloft}

     8 \addtolength\cftsubsecnumwidth {0.5em}

     9 \addtolength\cftsubsubsecnumwidth {1.0em}

    10

    11 \begin{document}

    12

    13 \title{The Constructible Universe\\ and the\\

    14        Relative Consistency of the Axiom of Choice}

    15 \author{Lawrence C Paulson}

    16 \maketitle

    17

    18 \begin{abstract}

    19   G\"odel's proof of the relative consistency of the axiom of

    20   choice~\cite{goedel40} is one of the most important results in the

    21   foundations of mathematics. It bears on Hilbert's first problem, namely the

    22   continuum hypothesis, and indeed G\"odel also proved the relative

    23   consistency of the continuum hypothesis. Just as important, G\"odel's proof

    24   introduced the \emph{inner model} method of proving relative consistency,

    25   and it introduced the concept of \emph{constructible

    26     set}. Kunen~\cite{kunen80} gives an excellent description of this body of

    27   work.

    28

    29   This Isabelle/ZF formalization demonstrates G\"odel's claim that his proof

    30   can be undertaken without using metamathematical arguments, for example

    31   arguments based on the general syntactic structure of a formula. Isabelle's

    32   automation replaces the metamathematics, although it does not eliminate the

    33   requirement at least to state many tedious results that would otherwise be

    34   unnecessary.

    35

    36   This formalization~\cite{paulson-consistency} is by far the deepest result

    37   in set theory proved in any automated theorem prover. It rests on a previous

    38   formal development of the reflection theorem~\cite{paulson-reflection}.

    39 \end{abstract}

    40

    41 \tableofcontents

    42

    43 \begin{center}

    44   \includegraphics[scale=0.7]{session_graph}

    45 \end{center}

    46

    47 \newpage

    48

    49 \parindent 0pt\parskip 0.5ex

    50

    51 \input{session}

    52

    53 \bibliographystyle{plain}

    54 \bibliography{root}

    55

    56 \end{document}