summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

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}

6 %table of contents is too crowded!

7 \usepackage{tocloft}

8 \addtolength\cftsubsecnumwidth {0.5em}

9 \addtolength\cftsubsubsecnumwidth {1.0em}

11 \begin{document}

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

14 Relative Consistency of the Axiom of Choice}

15 \author{Lawrence C Paulson}

16 \maketitle

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.

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.

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}

41 \tableofcontents

43 \begin{center}

44 \includegraphics[scale=0.7]{session_graph}

45 \end{center}

47 \newpage

49 \parindent 0pt\parskip 0.5ex

51 \input{session}

53 \bibliographystyle{plain}

54 \bibliography{root}

56 \end{document}