diff --git a/inputs/lecture_04.tex b/inputs/lecture_04.tex index 20bd08d..05005a2 100644 --- a/inputs/lecture_04.tex +++ b/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 diff --git a/inputs/lecture_07.tex b/inputs/lecture_07.tex index 1595c4e..9ba791b 100644 --- a/inputs/lecture_07.tex +++ b/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} - diff --git a/inputs/lecture_08.tex b/inputs/lecture_08.tex new file mode 100644 index 0000000..6685ed5 --- /dev/null +++ b/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 + + + + + + + diff --git a/jrpie-yaref.sty b/jrpie-yaref.sty index 00ab46b..d7cad52 100644 --- a/jrpie-yaref.sty +++ b/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% +} diff --git a/logic.sty b/logic.sty index 20f5018..9b5efa9 100644 --- a/logic.sty +++ b/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} diff --git a/logic2.tex b/logic2.tex index 9f99611..47d53e4 100644 --- a/logic2.tex +++ b/logic2.tex @@ -31,6 +31,7 @@ \input{inputs/lecture_05} \input{inputs/lecture_06} \input{inputs/lecture_07} +\input{inputs/lecture_08} \cleardoublepage