% -*- TeX:EN -*- %%% ==================================================================== %%% @LaTeX-file qedeq_set_theory_v1_1.00.00.tex %%% Generated at 2005-12-29 19:35:56,609 %%% ==================================================================== %%% Permission is granted to copy, distribute and/or modify this document %%% under the terms of the GNU Free Documentation License, Version 1.2 %%% or any later version published by the Free Software Foundation; %%% with no Invariant Sections, no Front-Cover Texts, and no Back-Cover Texts. \documentclass[a4paper,german,10pt,twoside]{book} \usepackage[english]{babel} \usepackage{makeidx} \usepackage{amsmath,amsthm,amssymb} \usepackage{color} \usepackage[bookmarks,bookmarksnumbered,bookmarksopen, colorlinks,linkcolor=webgreen,pagebackref]{hyperref} \definecolor{webgreen}{rgb}{0,.5,0} \usepackage{graphicx} \usepackage{xr} \usepackage{epsfig,longtable} \usepackage{tabularx} \newtheorem{thm}{Theorem}[chapter] \newtheorem{cor}[thm]{Corollary} \newtheorem{lem}[thm]{Lemma} \newtheorem{prop}[thm]{Proposition} \newtheorem{ax}{Axiom} \newtheorem{rul}{Rule} \theoremstyle{definition} \newtheorem{defn}[thm]{Definition} \newtheorem{idefn}[thm]{Initial Definition} \theoremstyle{remark} \newtheorem{rem}[thm]{Remark} \newtheorem*{notation}{Notation} \addtolength{\textheight}{7\baselineskip} \addtolength{\topmargin}{-5\baselineskip} \setlength{\parindent}{0pt} \frenchspacing \sloppy \makeindex \title{Axiomatic Set Theory} \author{ Michael Meyling } \begin{document} \maketitle \setlength{\parskip}{0pt} \tableofcontents \setlength{\parskip}{5pt plus 2pt minus 1pt} \chapter*{Preface\label{ch:preface}} \label{chapter0} \addcontentsline{toc}{chapter}{Preface\label{ch:preface}} Mathematics is a science with a structure that achieved enormous dimensions in the course of time. This huge stronghold has only a small set theoretic foundation and its firmness rests upon simple predicate calculus mortar. In principle the assembly could be comprehended by any mathematician. From every newest turret of mathematical cognition each path of logical dependency could be followed all the way down to the set theoretic roots. \par +++ missing translation \par Lets start by the roots\ldots \par This document is not finished and is updated from time to time. Especially at the locations marked with {\glqq+++\grqq} additions or changes will be made. \par I am deeply grateful to my wife \emph{Gesine~Dr{\"a}ger} and our son \emph{Lennart} for their support and patience. \par \vspace*{1cm} Hamburg, december 2005 \\ \hspace*{\fill} Michael Meyling %% end of chapter Preface\label{ch:preface} \chapter*{Introduction\label{ch:introduction}} \label{chapter1} \addcontentsline{toc}{chapter}{Introduction\label{ch:introduction}} \par +++ Translation missing This document contains the mathematical foundation of set theory. Goal is the presentation of elementary results which are needed within other mathematical disciplines. After the basics the {\emph boolean algebra of classes} is in focus. Next are some thoughts about \emph{relations} and \emph{functions}. An importent achievement is the definition of the \emph{natural~ numbers} and their fulfilment of the \emph{Peano axioms}. Also the word \emph{recursion} is discussed. \par Although the presentation is axiomatic the results shall match the mathematical usage. Therefore the set theoretic axiom system of \emph{A.~P.~Morse} and \emph{J.~L.~Kelley} (MK\index{MK}) was choosen. %% end of chapter Introduction\label{ch:introduction} \chapter{Basics} \label{chapter2} In this chapter we start with the very basic axioms and definitions of set theory. We shall make no attempt to introduce a formal language but shall be content with the common logical operators. To be more precise: precondition is a first-order predicate calculus with identity. \par\index{Cantor}\index{set!definition} \emph{G.~Cantor}, who is considered the founder of set theory, gave in a publication in 1895 a description of the term \emph{set}. \begin{quote} By a ``set'' we are to understand any collection into a whole $M$ of definite and separate objects $m$ of our intuition or our thought. These objects are called the ``elements'' of $M$. \end{quote} \par This collection can be specified by giving a \emph{condition for memberschip}. Around 1900 various paradoxes in this naive set theory were discovered. These paradoxes base on giving tricky conditions for membership. \par There exist different ways out of those contradictions. In this text we don't restrict the condition for membership but we call the result \emph{class}. Additional axioms allow us to call certain classes sets again. All sets are classes, but not all classes are sets. Sets are classes which are themselves members of classes, whilst a class which is not a set is a class which is not a member of any class. \section{Classes and Sets} \label{section0} Although we want to speak about \emph{sets} at the very beginning we have \emph{classes}. No formal definition of a class will be given. Informally, a class is a collection of objects, the involved objects are called the elements or members of the class. Sets will be construed as a special kind of class. The following definitions and axioms are due to a strengthened version of \emph{von~Neumann-Bernays-G{\"o}del's} set theory (\emph{NBG}\index{NBG}). This version is called \emph{MK}\index{MK} which is short for \emph{Morse-Kelley}. The theory of sets introduced here has initial objects, called \emph{classes}. Furthermore the only predefined symbol is for a binary relation called \emph{membership}. \par \begin{idefn}[Membership Operator] \label{in} $$x \in y$$ \end{idefn} We also say $x$ \emph{is element of} $y$, $x$ \emph{belongs to} $y$, $x$ \emph{is a member of} $y$, $x$ \emph{is in} $y$. Beside identity this is the only predicate we start with. All other will be defined.\footnote{One could also define the identity predicate within the set theory, but then another axiom is needed and the theory presentation is not so smooth for technical reasons (derivation of the equality axioms).} Also no function constants are initially given. Although we simply can negate the membership predicate we also want to define a shorthand notation for it. \par \begin{defn}[Non Membership Operator] \label{notIn} $$x \notin y\ := \ \neg x \in y$$ \end{defn} Our first axiom states that, for any classes $x$ and $y$, if the membership of $x$ and $y$ are the same, then $x$ and $y$ are the same.\footnote{If identity were not part of our underlying logic, then we should need to take this as a definition of identity.} \par \begin{ax}[Extensionality\index{axiom!of extensionality}] \label{axiom:extensionality} \mbox{} \begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}} $\forall z\ (z \in x\ \leftrightarrow \ z \in y)\ \rightarrow \ x \ = \ y$ \end{longtable} \end{ax} The classes $x$ and $y$ may be defined in entirely different ways, for example: \par \begin{tabularx}{\linewidth}{rcX} $x$ & = & class of all nonnegative integers, \\ $y$ & = & class of all integers, that can be written as sum of four squares, \end{tabularx} \par but if they have the same members, they are the same class. Now we specify \emph{sets}. \par \begin{defn}[Set\index{set!definition}] \label{isSet} $$\mathfrak{M}(x)\ := \ \exists y\ x \in y$$ \end{defn} So sets are nothing else than special classes. A class is a set iff it is a member of any class. As a consequence of the axiom of extensionality we have the following.\footnote{The quantification over $z$ is restricted to sets.} \par \begin{prop} \label{theorem:extensionalitySetRestricted} \mbox{} \begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}} $\forall \ \mathfrak{M}(z)\ (z \in x\ \leftrightarrow \ z \in y)\ \rightarrow \ x \ = \ y$ \end{longtable} \end{prop} \begin{proof} Assume $\forall \ \mathfrak{M}(z) \ ( z \in x \ \leftrightarrow \ z \in y)$. Let $z$ be an arbitrary class. If $z \in x$ then $z$ is a set by definition~\ref{isSet}, and hence by the assumption, $z \in y$. Similarly $z \in y \ \rightarrow \ z \in x$. Since $z$ is arbitrary, it follows that $\forall z \ (z \in x \ \leftrightarrow \ z \in y)$. Thus by the axiom of extensionality~\ref{axiom:extensionality}, $x = y$. \end{proof} We can also reverse the implication in the axiom of extensionality. \par \begin{prop} \label{theorem:extensonalityEquivalence} \mbox{} \begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}} $x \ = \ y\ \leftrightarrow \ \forall z\ (z \in x\ \leftrightarrow \ z \in y)$ \end{longtable} \end{prop} \begin{proof} This a simple consequence of the second identity axiom. \end{proof} Our second axiom makes it simple to create new classes. A class could be characterized by a predicate calculus formula. \par \begin{ax}[Comprehension] \label{axiom:comprehension} \mbox{} \begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}} $\exists x\ \forall y\ (x \in y\ \leftrightarrow \ (\mathfrak{M}(y)\ \land \ \phi(y)))$ \end{longtable} \end{ax} \index{NBG}By modifying the above axiom we could get a \emph{NBG} axiom system of set theory due to \emph{John von Neumann}, \emph{Isaak Bernays} and \emph{Kurt G{\"o}del}. \par\index{predicative}\index{Formula, predicative} For that purpose we call a formula \emph{predicative}, if all of its bound subject variables are restricted to sets. Therefore predicative formulas formalize `set properties'.\footnote{A little bit more formal: within a predicative formula all quantifier variables run over sets: $\forall \ \mathfrak{M}(x) \ \exists \ \mathfrak{M}(y) \ldots$} So if we postulate $\phi$ to be predicative we achieve a NBG system in the following. By the comprehension axiom and the axiom of extensionality a relationship between a sentence $\phi(y)$ and the class defined by this sentence is described. The comprehension axiom proposes the existence of at least one class, where the sentence $\mathfrak{M}(y) \land \phi(y)$ holds for all elements. The axiom of extensionality and the identity axioms make sure, that there is maximal one class of this kind: two classes with the same elements are equal in the sense of replacement in all appropriate sentences. In other words: there is one and only one such class. \par \begin{prop} \label{theorem:comprehension} \mbox{} \begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}} $\exists! x\ \forall y\ (x \in y\ \leftrightarrow \ (\mathfrak{M}(y)\ \land \ \phi(y)))$ \end{longtable} \end{prop} \begin{proof} We must show: $$ \begin{array}{rl} \exists x & \forall y \ (y \in x \leftrightarrow \ \mathfrak{M}(y) \land \phi(y)) \\ \land \ \forall u \ \forall v & (\forall y \ (y \in u \leftrightarrow \mathfrak{M}(y) \land \phi(y)) \ \land \ \forall y \ ( y \in v \leftrightarrow \ \mathfrak{M}(y) \land \phi(y))) \\ & \qquad \rightarrow u = v) \end{array} $$ Let $u$ and $v$ be arbitrary. Furthermore let us assume: \par $\forall y \ (y \in u \leftrightarrow \ \mathfrak{M}(y) \land \phi(y)) \land \ \forall y \ ( y \in v \leftrightarrow \mathfrak{M}(y) \land \phi(y)))$ \par Now with \ref{allandpp}: $\forall y \ ((y \in u \leftrightarrow \mathfrak{M}(y) \land \phi(y)) \land (y \in v \leftrightarrow \mathfrak{M}(y) \land \phi(y)))$ \par With \ref{andequi} we derive: $\forall y \ ((y \in u \leftrightarrow y \in v ))$. And with Proposition~\ref{theorem:extensonalityEquivalence} follows $u = v$. So we have shown: \par $\forall u \ \forall v \ (\forall y \ (y \in u \leftrightarrow \mathfrak{M}(y) \land \phi(y)) \land \ \forall y \ (y \in v \leftrightarrow \mathfrak{M}(y) \land \phi(y))) \rightarrow u = v)$ \par Together with axiom~\ref{axiom:comprehension} we get the proposition. \end{proof} Starting with \ref{theorem:comprehension} we can extend the syntax and provide a new abbreviation. \par \begin{rul}[Class definition] \label{rule:classDefinition} For every formula $\alpha(x)$ we define the term expression $\{ x \ | \ \alpha(x)\}$ by $$ \exists y \ (y = \{x \ | \ \alpha(x) \} \ \land \ \forall x \ x \in y \ \leftrightarrow \mathfrak{M}(x) \ \land \alpha(x)) $$ \par The free variables from $\{ x \ | \ \alpha(x)\}$ are the free variables from $\alpha(x)$ without $\{ x \}$. The bound variables correspond to the bound variables of $\alpha(x)$. All deduction rules are accordingly extended. \end{rul} In particular the substitution rule must be adapted. This is a \emph{conservative} extension. This new notation can be easily transformed in the old syntax. Using the new term type with the initial predicates can be expressed as follows. \par \begin{prop} \label{theorem:setNotation} \mbox{} \begin{longtable}{{@{\extracolsep{\fill}}p{\linewidth}}} $(y \in \{ x \ | \ \phi(x) \} \ \leftrightarrow \ (\mathfrak{M}(y)\ \land \ \phi(y)))\ \land \ (y \ = \ \{ x \ | \ \phi(x) \} \ \leftrightarrow \ \forall z\ (z \in y\ \leftrightarrow \ z \in \{ x \ | \ \phi(x) \} ))\ \land \ (\{ x \ | \ \phi(x) \} \ = \ \{ x \ | \ \psi(x) \} \ \leftrightarrow \ \forall z\ (z \in \{ x \ | \ \phi(x) \} \ \leftrightarrow \ z \in \{ x \ | \ \psi(x) \} ))\ \land \ (\{ x \ | \ \phi(x) \} \in \{ x \ | \ \psi(x) \} \ \leftrightarrow \ \forall u\ \forall v\ ((u \ = \ \{ x \ | \ \phi(x) \} \ \land \ v \ = \ \{ x \ | \ \psi(x) \} )\ \rightarrow \ u \in v))\ \land \ (\{ x \ | \ \phi(x) \} \in y\ \leftrightarrow \ \forall u\ (u \ = \ \{ x \ | \ \phi(x) \} \ \rightarrow \ u \in v))$ \end{longtable} +++ if the formula would be rendered it should look like this: \\ \begin{align} y \in \{ x~|~\phi(x) \} & \leftrightarrow \mathfrak{M}(y) \land \phi(y) \tag{a} \\ y = \{ x~|~ \phi(x) \} & \leftrightarrow \forall z \ (z \in y \leftrightarrow z \in \{ x~|~\phi(x) \}) \tag{b} \\ \{ x~|~\phi(x) \} = \{ x~|~\psi(x) \} & \leftrightarrow \forall z \ (z \in \{ x~|~\phi(x) \} \tag{c} \\ \begin{split} & \qquad \leftrightarrow z \in \{x~|~\psi(x) \}) \nonumber \\ \{ x~|~\phi(x) \} \in \{ x~|~\psi(x) \} & \leftrightarrow \forall u \ \forall v \ ((u = \{ x~|~\phi(x) \} \\ & \qquad \land \ v = \{ x~|~\psi(x) \}) \rightarrow u \in v) \end{split} \tag{d} \\ \{ x~|~\phi(x) \} \in y & \leftrightarrow \forall u \ (u = \{ x~|~\phi(x) \} \rightarrow u \in y) \tag{e} \end{align} \end{prop} \begin{proof} +++ missing. \end{proof} Therefore the new syntax can be eliminated by successive applying the above theorems. %% end of chapter Basics \backmatter \addcontentsline{toc}{chapter}{\indexname} \printindex \end{document}