TODO

inputs/lecture_04.tex

@@ -32,6 +32,7 @@ $\ZFC$ stands for
 \end{notation}
 $\ZFC$ consists of the following axioms:
 \begin{axiom}[\vocab{Extensionality}]
+    \yalabel{Axiom of Extensionality}{(AoE)}{ax:ext}
     \[
     \forall x.~\forall y.~(x = y \iff \forall z.~(z \in x \iff z \in y)).
     \]
@@ -42,6 +43,7 @@ $\ZFC$ consists of the following axioms:
 \end{axiom}
 
 \begin{axiom}[\vocab{Foundation}]
+    \yalabel{Axiom of Foundation}{(Fund)}{ax:fund}
     Every set has an $\in$-minimal member:
     \[
     \forall  x .~ \left(\exists  a .~(a\in x) \implies
@@ -53,6 +55,7 @@ $\ZFC$ consists of the following axioms:
     \]
 \end{axiom}
 \begin{axiom}[\vocab{Pairing}]
+    \yalabel{Axiom of Pairing}{(Pair)}{ax:aop} % AoP
     \[
     \forall x .~\forall y.~ \exists z.~(z = \{x,y\}).
     \]
@@ -72,12 +75,14 @@ $\ZFC$ consists of the following axioms:
 \end{remark}
 
 \begin{axiom}[\vocab{Union}]
+    \yalabel{Axiom of Union}{(AoU)}{ax:union} % Union
     \[
     \forall x.~\exists y.~(y = \bigcup x).
     \]
 \end{axiom}
 
 \begin{axiom}[\vocab{Powerset}]
+    \yalabel{Powerset Axiom}{(Pow)}{ax:pow}
     We write $x = \cP(y)$
     for
     $\forall  z.~(z \in x \iff x \subseteq z)$.
@@ -87,13 +92,14 @@ $\ZFC$ consists of the following axioms:
     \]
 \end{axiom}
 \begin{axiom}[\vocab{Infinity}]
+    \yalabel{Axiom of Infinity}{(Inf)}{ax:inf}
     A set $x$ is called \vocab{inductive},
     iff $\emptyset \in x \land \forall y.~(y \in x \implies y \cup \{y\} \in x)$.
 
     The axiom of infinity says that there exists and inductive set.
 \end{axiom}
-
 \begin{axiomschema}[\vocab{Separation}]
+    \yalabel{Axiom Schema of Separation}{(Aus)}{ax:aus}
     % TODO :(Aus)
     Let $\phi$ be some fixed
     fist order formula in $\cL_\in$.
@@ -143,6 +149,3 @@ $\ZFC$ consists of the following axioms:
                     &)&
     \end{IEEEeqnarray*}
 \end{axiom}
-
-
-% TODO Hier weiter

inputs/lecture_07.tex

@@ -192,9 +192,4 @@ for example $\bigcup \omega = \omega$.
         \item $1 = \{0\}, 2 = \{0,1\}, 3, \ldots$
         \item $\omega +1 = \omega \cup \{\omega\} , \omega + 2, \ldots$,
     \end{itemize}
-    
-    
 \end{example}
-
-\subsection{Induction and Recursion}
-

inputs/lecture_08.tex

@@ -0,0 +1,239 @@
+\lecture{08}{2023-11-13}{Induction and recursion}
+
+\subsection{Classes}
+It is often very handy to work in a class theory rather than
+in set theory.
+
+To formulate a class theory,
+we start out with a first order language
+with two types of variables,
+sets (denoted by lower case letters)
+and classes (denoted by capital letters),
+as well as one binary relation symbol $\in$
+for membership.
+
+\vocab{Bernays-Gödel class theory} (\vocab{BG})
+has the following axioms:
+
+\begin{axiom}[Extensionality]
+    \yalabel{Axiom of Extensionality}{(Ext)}{ax:bg:ext}
+    \[
+    \forall x, y. \left( x = y \iff \left( \forall z.~(z \in x \iff z \in y \right)  \right).
+    \] 
+\end{axiom}
+\begin{axiom}[Foundation]
+    \yalabel{Axiom of Foundation}{(Fund)}{ax:bg:fund}
+    \[
+    \forall x .(x \neq \emptyset \implies \exists  y \in x . y \cap x = \emptyset).
+    \] 
+\end{axiom}
+
+\begin{axiom}[Pairing]
+    \yalabel{Axiom of Pairing}{(Pair)}{ax:bg:pair}
+    \[
+    \forall x \forall  y \exists  z . z = \{x,y\}.
+    \] 
+\end{axiom}
+
+\begin{axiom}[Union]
+    \yalabel{Axiom of Union}{(Union)}{ax:bg:union}
+    \[
+    \forall  x \exists  y .~ y = \bigcup x.
+    \] 
+\end{axiom}
+\begin{axiom}[Power]
+    \yalabel{Powerset Axiom}{(Pow)}{ax:bg:pow}
+    \[
+    \forall x \exists  y .~ y = \cP(x).
+    \] 
+\end{axiom}
+
+\begin{axiom}[Infinity]
+    \yalabel{Axiom of Infinity}{(Infinity)}{ax:bg:inf}
+    \[
+    \exists  x . ~(\emptyset \in x \land \left( \forall y \in x .~y \cup \{y\}  \in x \right)).
+    \] 
+\end{axiom}
+
+Together with the following axioms for classes:
+
+\begin{axiom}[Extensionality for classes]
+    \[
+        \forall X \forall  Y \left( \forall  x(x \in X \iff y \in X) \implies X = Y).
+    \] 
+\end{axiom}
+
+\begin{axiom}
+    Every set is a class:
+    \[
+    \forall  x \exists X. x = X.
+    \] 
+\end{axiom}
+\begin{axiom}
+    Every element of a class is a set:
+    \[
+        \forall X \exists Y.~(X \in Y \to  \exists x.~x = X).
+    \] 
+\end{axiom}
+\begin{axiom}[Replacement]
+    \yalabel{Axiom of Replacement}{(Rep)}{ax:bg:rep}
+
+    If $F$ is a function and inf $a $ is a set,
+    then $F"a$ is a set.
+\end{axiom}
+Here a \vocab[Class function]{(class) function} is a class
+consisting of pairs $(x,y)$,
+such that for every  $x$ there is at most one $y$
+with $(x,y) \in F$.
+Furthermore $F"a \coloneqq  \{y : \exists  x \in  a .~(x,y) \in F\}$.
+
+\begin{remark}
+    Note that we didn't need to use an axiom schema,
+    \yarefs{ax:bg:rep} is a single axiom.
+\end{remark}
+
+\begin{axiom}[Comprehension]
+    \yalabel{Axiom of Comprehension}{(Comp)}{ax:bg:comp}
+
+    \[
+    \forall X_1 \ldots \forall X_k .~\exists Y ( \forall  x .~x \in Y \iff \phi(x,X_1,\ldots, X_k))
+    \] 
+    where $\phi(x, X_1, \ldots, X_k)$
+    is a formula which contains exactly $X_1, \ldots, X_k, x$
+    as free variables,
+    and $\phi$ does not have quantifiers
+    ranging over classes.%
+    \footnote{If one removes the restriction regarding
+        quantifiers another theory, called
+        \vocab{Morse-Kelly} set theory, is obtained.}
+\end{axiom}
+
+
+\todo{notation: $\emptyset, \cap$}
+
+
+
+\subsection{Induction and Recursion}
+
+\begin{definition}
+    A binary relation $R$ on a set $X$,
+    i.e.~$R \subseteq X \times X$,
+    is called \vocab{well-founded}
+    iff for all $\emptyset \neq Y \subseteq X$
+    there is some $x \in Y$
+    such that for no $y \in Y. (y,x) \in R$.
+\end{definition}
+
+\begin{example}
+    \begin{enumerate}[(a)]
+        \item $(\N, <)$ is well-founded.
+        \item Let $M$ be a set,
+            and let $\in\defon{M} \coloneqq  \{(x,y) : x,y \in M \land x \in y\}$.
+            Fund is equivalent to saying that
+            this is a well-founded relation for every $M$.
+    \end{enumerate}
+\end{example}
+
+
+\begin{lemma}
+    \label{lem:fundseq}
+    In $\ZFC - \Fund$,
+    the following are equivalent:
+    \begin{itemize}
+        \item \Fund,
+        \item There is no sequence $\langle x_n : n < \omega \rangle$
+             such that $x_{n+1} \in x_n$ for all $n < \omega$.
+    \end{itemize}
+\end{lemma}
+\begin{proof}
+    Suppose such sequence exists.
+    Then $\{x_n : n < \omega\}$
+    (this exists as by definition sequence of the $x_n$ is a function
+    and this set is the range of that function)
+    violates \Fund.
+
+    For the other direction let $M \neq \emptyset$ be some set.
+    Suppose that \Fund does not hold for $M$.
+
+    Using \Choice,
+    we construct an infinite sequence $x_0 \ni x_1 \ni x_2 \ni \ldots$
+    of elements of $M$.
+
+    More formally,
+    for each $x \in M$
+    let $A_x \coloneqq  \{y \in M: y \in x\}$.
+    Suppose that $A_x \neq \emptyset$ for all $x \in M$.
+    Using \AxC
+    we get a function for $\langle A_x : x \in M \rangle$,%
+    \footnote{Actually we only need the axiom of dependent choice,
+        a weaker form of the axiom of choice.
+        We'll discuss this later.% TODO REF
+    }
+    i.e.~a function $f\colon M \to  M$
+    such that $f(x) \in A_x$ for $x \in M$.
+    Now fix $x \in M$.
+    We want to produce
+    a function
+    $g\colon \omega \to  M$
+    such that
+    \begin{itemize}
+        \item $g(0) = x$,
+        \item $g(n+1) = f(g(n)) \in A_{g(n)}$.
+    \end{itemize}
+
+    Let
+    \begin{IEEEeqnarray*}{rCl}
+        G &=& \{\overline{g} : \exists  n \in  \omega . \\
+          &&~ ~\overline{g} \text{ is a function with domain $n$ and range $\subseteq  M$, such that}\\
+          &&~ ~\overline{g}(0) = x \land \forall m \in  \omega.~(m+1 \in \dom(\overline{g}) \implies \overline{g}(m+1) = f(\overline{g}(m)))\}.
+    \end{IEEEeqnarray*}
+    $G$ exists as it can be obtained by \AxSep
+    from ${}^{< \omega}M$.
+    By induction,
+    for every $n \in  \omega$,
+    there is a $\overline{g} \in G$
+    with $\dom(\overline{g}) \in n+1$:
+    This holds for $n = 0$,
+    as $\{(0,x)\} \in  G$.
+    If $\overline{g} \in  G$ with $\dom(\overline{g}) = n+ 1$,
+    then $\overline{g} \cup  \{(n+1, f(\overline{g}(n)))\} \in G$.
+    Also by induction,
+    for every $n \in \omega$,
+    there is a \emph{unique}
+    $\overline{g}$ with $\dom(\overline{g}) = n+1$.
+
+    Now let $g = \bigcup \overline{G}$.
+    Also let $g(0) = x$ and $g(n+1) = f(g(n))$
+    for all  $n \in \omega$.
+\end{proof}
+
+\begin{lemma}[Dependent Choice]
+    Suppose that $M \neq  \emptyset$
+    and $R$ is a binary relation on $M$
+    such that for all $x \in M$,
+    $A_x \coloneqq  \{y \in M : (y,x) \in R\}$
+    is not empty.
+
+    Then for every $x \in M$ there exists a function
+    $g\colon \omega \to M$
+    such that $g(0) = x$
+    and $g(n+1) \in A_{g(n)}$
+    for all $n < \omega$.
+\end{lemma}
+\begin{proof}
+    We showed a special case of this in the proof of
+    \yaref{lem:fundseq}.
+\end{proof}
+\begin{remark}
+    In $\ZF$ this is a weaker form of \Choice.
+\end{remark}
+
+The construction of $g$ in the previous proof was a special case of
+a construction on the proof of the recursion theorem: % TODO REF
+
+
+
+
+
+
+

jrpie-yaref.sty

@@ -47,3 +47,11 @@
         \yaref@text@large{#1}%
     \fi%
 }
+% Force a small reference
+\newcommand{\yarefs}[1]{%
+    \relax\ifmmode%
+        \yaref@math@verysmall{#1}  % scriptscript style
+    \else%
+        \yaref@text@small{#1} %
+    \fi%
+}

logic.sty

@@ -113,7 +113,10 @@
 \DeclareSimpleMathOperator{HOD}
 \DeclareSimpleMathOperator{OD}
 \DeclareSimpleMathOperator{AC}
-\DeclareSimpleMathOperator{Fund}
+\newcommand{\Choice}{\yarefs{ax:c}}
+% \DeclareSimpleMathOperator{Choice}
+% \DeclareSimpleMathOperator{Fund}
+\newcommand{\Fund}{\yarefs{ax:fund}}
 \DeclareSimpleMathOperator{Pair}
 \DeclareSimpleMathOperator{Union}
 \DeclareSimpleMathOperator{Rep}
@@ -124,7 +127,6 @@
 \DeclareSimpleMathOperator{AoP}
 \DeclareSimpleMathOperator{AoU}
 \DeclareSimpleMathOperator{AoI}
-\DeclareSimpleMathOperator{Choice}
 \DeclareSimpleMathOperator{Inf}
 
 

logic2.tex

@@ -31,6 +31,7 @@
 \input{inputs/lecture_05}
 \input{inputs/lecture_06}
 \input{inputs/lecture_07}
+\input{inputs/lecture_08}
 
 
 \cleardoublepage

todo

@@ -0,0 +1 @@
+Better REF for axioms