src/ZF/AC/document/root.tex
author wenzelm
Wed, 23 Jul 2025 14:53:21 +0200
changeset 82898 89da4dcd1fa8
parent 73404 299f6a8faccc
permissions -rw-r--r--
clarified colors, following d6a14ed060fb;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
15083
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
     1
\documentclass[11pt,a4paper]{article}
73404
299f6a8faccc proper type-setting of cartouches (requires T1);
wenzelm
parents: 17159
diff changeset
     2
\usepackage[T1]{fontenc}
15083
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
     3
\usepackage{graphicx}
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
     4
\usepackage{isabelle,amssymb,isabellesym}
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
     5
\usepackage{pdfsetup}\urlstyle{rm}
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
     6
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
     7
%table of contents is too crowded!
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
     8
\usepackage{tocloft}
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
     9
\addtolength\cftsubsecnumwidth {0.5em}
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    10
\addtolength\cftsubsubsecnumwidth {1.0em}
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    11
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    12
\begin{document}
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    13
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    14
\title{Equivalents of the Axiom of Choice}
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    15
\author{Krzysztof Gr\c{a}bczewski}
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    16
\maketitle
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    17
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    18
\begin{abstract}
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    19
  This development~\cite{paulson-gr} proves the equivalence of seven
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    20
  formulations of the well-ordering theorem and twenty formulations of the
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    21
  axiom of choice. It formalizes the first two chapters of the monograph
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    22
  \emph{Equivalents of the Axiom of Choice} by Rubin and
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    23
  Rubin~\cite{rubin&rubin}. Some of this mmaterial involves extremely complex
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    24
  techniques.
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    25
\end{abstract}
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    26
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    27
\tableofcontents
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    28
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    29
\begin{center}
17159
d5060118122e tuned size of included graph;
wenzelm
parents: 15083
diff changeset
    30
  \includegraphics[width=\textwidth]{session_graph}
15083
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    31
\end{center}
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    32
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    33
\newpage
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    34
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    35
\parindent 0pt\parskip 0.5ex
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    36
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    37
\input{session}
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    38
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    39
\bibliographystyle{plain}
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    40
\bibliography{root}
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    41
a471fd1d9961 documents for ZF-AC and ZF-Constructible
paulson
parents:
diff changeset
    42
\end{document}