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}