src/ZF/Constructible/document/root.tex
author paulson
Thu Jul 29 12:15:53 2004 +0200 (2004-07-29)
changeset 15083 a471fd1d9961
parent 13721 2cf506c09946
permissions -rw-r--r--
documents for ZF-AC and ZF-Constructible
wenzelm@13295
     1
\documentclass[11pt,a4paper]{article}
wenzelm@13427
     2
\usepackage{graphicx}
paulson@13543
     3
\usepackage{isabelle,amssymb,isabellesym}
wenzelm@13427
     4
\usepackage{pdfsetup}\urlstyle{rm}
wenzelm@13295
     5
paulson@15083
     6
%table of contents is too crowded!
paulson@13556
     7
\usepackage{tocloft}
paulson@13721
     8
\addtolength\cftsubsecnumwidth {0.5em}
paulson@13721
     9
\addtolength\cftsubsubsecnumwidth {1.0em}
wenzelm@13295
    10
wenzelm@13295
    11
\begin{document}
wenzelm@13295
    12
paulson@15083
    13
\title{The Constructible Universe\\ and the\\
paulson@15083
    14
       Relative Consistency of the Axiom of Choice}
wenzelm@13295
    15
\author{Lawrence C Paulson}
wenzelm@13295
    16
\maketitle
wenzelm@13295
    17
paulson@15083
    18
\begin{abstract}
paulson@15083
    19
  G\"odel's proof of the relative consistency of the axiom of
paulson@15083
    20
  choice~\cite{goedel40} is one of the most important results in the
paulson@15083
    21
  foundations of mathematics. It bears on Hilbert's first problem, namely the
paulson@15083
    22
  continuum hypothesis, and indeed G\"odel also proved the relative
paulson@15083
    23
  consistency of the continuum hypothesis. Just as important, G\"odel's proof
paulson@15083
    24
  introduced the \emph{inner model} method of proving relative consistency,
paulson@15083
    25
  and it introduced the concept of \emph{constructible
paulson@15083
    26
    set}. Kunen~\cite{kunen80} gives an excellent description of this body of
paulson@15083
    27
  work.
paulson@15083
    28
  
paulson@15083
    29
  This Isabelle/ZF formalization demonstrates G\"odel's claim that his proof
paulson@15083
    30
  can be undertaken without using metamathematical arguments, for example
paulson@15083
    31
  arguments based on the general syntactic structure of a formula. Isabelle's
paulson@15083
    32
  automation replaces the metamathematics, although it does not eliminate the
paulson@15083
    33
  requirement at least to state many tedious results that would otherwise be
paulson@15083
    34
  unnecessary.
paulson@15083
    35
  
paulson@15083
    36
  This formalization~\cite{paulson-consistency} is by far the deepest result
paulson@15083
    37
  in set theory proved in any automated theorem prover. It rests on a previous
paulson@15083
    38
  formal development of the reflection theorem~\cite{paulson-reflection}.
paulson@15083
    39
\end{abstract}
paulson@15083
    40
wenzelm@13295
    41
\tableofcontents
wenzelm@13295
    42
wenzelm@13427
    43
\begin{center}
wenzelm@13427
    44
  \includegraphics[scale=0.7]{session_graph}
wenzelm@13427
    45
\end{center}
wenzelm@13427
    46
wenzelm@13427
    47
\newpage
wenzelm@13427
    48
wenzelm@13295
    49
\parindent 0pt\parskip 0.5ex
wenzelm@13295
    50
wenzelm@13295
    51
\input{session}
wenzelm@13295
    52
paulson@15083
    53
\bibliographystyle{plain}
paulson@15083
    54
\bibliography{root}
wenzelm@13295
    55
wenzelm@13295
    56
\end{document}