inputs/lecture_04.tex

@@ -32,7 +32,6 @@ $\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)).
     \]
@@ -43,7 +42,6 @@ $\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
@@ -55,7 +53,6 @@ $\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\}).
     \]
@@ -75,14 +72,12 @@ $\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)$.
@@ -92,14 +87,13 @@ $\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$.
@@ -149,3 +143,6 @@ $\ZFC$ consists of the following axioms:
                     &)&
     \end{IEEEeqnarray*}
 \end{axiom}
+
+
+% TODO Hier weiter

inputs/lecture_07.tex

@@ -192,4 +192,9 @@ 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

@@ -1,239 +0,0 @@
-\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,11 +47,3 @@
         \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,10 +113,7 @@
 \DeclareSimpleMathOperator{HOD}
 \DeclareSimpleMathOperator{OD}
 \DeclareSimpleMathOperator{AC}
-\newcommand{\Choice}{\yarefs{ax:c}}
+\DeclareSimpleMathOperator{Fund}
-% \DeclareSimpleMathOperator{Choice}
-% \DeclareSimpleMathOperator{Fund}
-\newcommand{\Fund}{\yarefs{ax:fund}}
 \DeclareSimpleMathOperator{Pair}
 \DeclareSimpleMathOperator{Union}
 \DeclareSimpleMathOperator{Rep}
@@ -127,6 +124,7 @@
 \DeclareSimpleMathOperator{AoP}
 \DeclareSimpleMathOperator{AoU}
 \DeclareSimpleMathOperator{AoI}
+\DeclareSimpleMathOperator{Choice}
 \DeclareSimpleMathOperator{Inf}
 
 

logic2.tex

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

todo

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