diff --git a/inputs/lecture_04.tex b/inputs/lecture_04.tex index 641184f..6f12fa5 100644 --- a/inputs/lecture_04.tex +++ b/inputs/lecture_04.tex @@ -28,11 +28,11 @@ $\ZFC$ stands for Let $x = \bigcup y$ denote \[ \forall z.~(z \in x \iff \exists v.(v \in y \land z \in v)). - \] + \] \end{notation} $\ZFC$ consists of the following axioms: \begin{axiom}[\vocab{Extensionality}] - \yalabel{Axiom of Extensionality}{(AoE)}{ax:ext} + \yalabel{Axiom of Extensionality}{(Ext)}{ax:ext} % (AoE) \[ \forall x.~\forall y.~(x = y \iff \forall z.~(z \in x \iff z \in y)). \] @@ -55,7 +55,7 @@ $\ZFC$ consists of the following axioms: \] \end{axiom} \begin{axiom}[\vocab{Pairing}] - \yalabel{Axiom of Pairing}{(Pair)}{ax:aop} % AoP + \yalabel{Axiom of Pairing}{(Pair)}{ax:pair} % AoP \[ \forall x .~\forall y.~ \exists z.~(z = \{x,y\}). \] @@ -75,18 +75,19 @@ $\ZFC$ consists of the following axioms: \end{remark} \begin{axiom}[\vocab{Union}] - \yalabel{Axiom of Union}{(AoU)}{ax:union} % Union + \yalabel{Axiom of Union}{(Union)}{ax:union} % Union (AoU) \[ \forall x.~\exists y.~(y = \bigcup x). \] \end{axiom} -\begin{axiom}[\vocab{Powerset}] - \yalabel{Powerset Axiom}{(Pow)}{ax:pow} +\begin{axiom}[\vocab{Power Set}] + \yalabel{Axiom of Power Set}{(Pow)}{ax:pow} + % (PWA) We write $x = \cP(y)$ for $\forall z.~(z \in x \iff x \subseteq z)$. - The powerset axiom (PWA) states + The power set axiom states \[ \forall x.~\exists y.~y=\cP(x). \] @@ -99,11 +100,11 @@ $\ZFC$ consists of the following axioms: 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) + \yalabel{Axiom of Separation}{(Aus)}{ax:aus} + Let $\phi$ be some fixed fist order formula in $\cL_\in$. - Then $\text{(Aus)}_{\phi}$ + Then $\AxAus_{\phi}$ states \[ \forall v_1 .~\forall v_p .~\forall a .~\exists b .~\forall x.~ @@ -112,7 +113,7 @@ $\ZFC$ consists of the following axioms: Let us write $b = \{x \in a | \phi(x)\}$ for $\forall x.~(x \in b \iff x \in a \land f(x))$. - Then (Aus) can be formulated as + Then \AxAus can be formulated as \[ \forall a.~\exists b.~(b = \{x \in a; \phi(x)\}). \] @@ -125,7 +126,7 @@ $\ZFC$ consists of the following axioms: % $x = \bigcap y$ for ... \end{notation} \begin{remark} - (Aus) proves that + \AxAus proves that \begin{itemize} \item $\forall a.~\forall b.~\exists c.~(c = a \cap b)$, \item $\forall a.~\forall b.~\exists c.~(c = a \setminus b)$, @@ -133,6 +134,7 @@ $\ZFC$ consists of the following axioms: \end{itemize} \end{remark} \begin{axiomschema}[\vocab{Replacement} (Fraenkel)] + \yalabel{Axiom of Replacement}{(Rep)}{ax:rep} Let $\phi$ be some $\cL_{\in }$ formula. Then \[ @@ -141,6 +143,7 @@ $\ZFC$ consists of the following axioms: \end{axiomschema} \begin{axiom}[\vocab{Choice}] + \yalabel{Axiom of Choice}{(C)}{ax:c} Every family of non-empty sets has a \vocab{choice set}: \begin{IEEEeqnarray*}{rCl} \forall x .~&(&\\ diff --git a/inputs/lecture_05.tex b/inputs/lecture_05.tex index 6434571..c421a29 100644 --- a/inputs/lecture_05.tex +++ b/inputs/lecture_05.tex @@ -2,24 +2,24 @@ \begin{definition} Zermelo: - \[\Zermelo \coloneqq \AoE + \AoF + \AoP + \AoU + \Pow + \AoI + \Aus_{\phi}\] + \[\Zermelo \coloneqq \AxExt + \AxFund + \AxPair + \AxUnion + \AxPow + \AxInf + \AxAus_{\phi}\] Zermelo and Fraenkl: \[ - {\ZF} \coloneqq Z + (\Rep_{\phi}) + {\ZF} \coloneqq Z + \AxRep_{\phi} % TODO fix parenthesis \] \[ - {\ZFC} \coloneqq \ZF + \Choice + {\ZFC} \coloneqq \ZF + \AxC \] Variants: \[ - {\ZFC^{-}} \coloneqq \ZFC \setminus \Pow. + {\ZFC^{-}} \coloneqq \ZFC \setminus \AxPow. \] \[ - {\ZFC^{-\infty}} \coloneqq \ZFC \setminus \Inf + {\ZFC^{-\infty}} \coloneqq \ZFC \setminus \AxInf \] \end{definition} @@ -37,12 +37,12 @@ we write \[ (x_1,\ldots,x_{n+1}) \coloneqq ((x_1,\ldots,x_n), x_{n+1}) - \] + \] where we assume that $(x_1,\ldots,x_{n})$ is already defined. \end{definition} \begin{definition} - The \vocab{cartesian product} + The \vocab{cartesian product} $a \times b$ of two sets $a$ and $b$ is defined to be $a \times b \coloneqq \{(x,y) | x \in a \land y \in b\}$. \end{definition} @@ -50,7 +50,7 @@ $a \times b$ exists. \end{fact} \begin{proof} - Use $\Aus$ over $\cP(\cP(a \cup b))$. + Use \AxAus over $\cP(\cP(a \cup b))$. \end{proof} \begin{definition} @@ -112,7 +112,7 @@ ${}^d b$ exists. \end{fact} \begin{proof} - Apply again $\Aus$ over $\cP(d \times b)$. + Apply again \AxAus over $\cP(d \times b)$. \end{proof} \begin{definition} diff --git a/inputs/lecture_06.tex b/inputs/lecture_06.tex index 5abfdab..5b68cd6 100644 --- a/inputs/lecture_06.tex +++ b/inputs/lecture_06.tex @@ -7,7 +7,7 @@ and $ b$ linearly ordered, $b$ has an upper bound, Then $a$ has a maximal element. \end{theorem} -\begin{proof} +\begin{refproof}{thm:zorn} Fix $(a, \le )$ as in the hypothesis. Let $A \coloneqq \{ \{(b,x) : x in b\} : b \le a, b \neq \emptyset\}$. Note that $A$ is a set (use separation on $\cP(\cP(a) \times \bigcup \cP(a))$). @@ -65,7 +65,7 @@ Then $B = B_{u_0}^{\le^{\ast\ast}}$. So $\le^{\ast\ast} \in W$, but now $n_0 \in b$. So $b$ must have a maximum. -\end{proof} +\end{refproof} \begin{remark} Over $\ZF$ the axiom of choice and \yaref{thm:zorn} @@ -107,20 +107,20 @@ of well-orders. % TODO theorem \end{goal} -Recall that (AoI) states the existence of an inductive set $x$. +Recall that \AxInf states the existence of an inductive set $x$. We can hence form the smallest inductive set \[ \omega \coloneqq \bigcap \{ x : x \text{ is inductive}\} \] Note that $\omega$ exists, as it is a subset of the inductive -set given by AoI. +set given by \AxInf. We call $\omega$ the set of \vocab{natural numbers}. \begin{notation} We write $0$ for $\emptyset$, and $y + 1$ for $y \cup \{y\}$. \end{notation} -With this notation the AoI is equivalent to +With this notation the \AxInf is equivalent to \[ \exists x_0.~(0 \in x_0 \land \forall n. ~(n \in x_0 \implies n+1 \in x_0)). \] @@ -218,7 +218,7 @@ Clearly, the $\in$-relation is a well-order on an ordinal $x$. \item In the first case, $z+1 = y+1$. \item Suppose that $z \in y$. Then by the induction hypothesis $\phi(y, z+1)$ holds. - If $y \in z+1$, then $\{y,z\}$ would violate AoF. + If $y \in z+1$, then $\{y,z\}$ would violate \AxFund. If $y = z+1$, then $z + 1 \in y + 1$. If $z+1 \in y$, then $z+1 \in y+1$ as well. \end{itemize} diff --git a/inputs/lecture_07.tex b/inputs/lecture_07.tex index 9ba791b..cf10aad 100644 --- a/inputs/lecture_07.tex +++ b/inputs/lecture_07.tex @@ -14,6 +14,7 @@ for ordinals. \end{notation} \begin{lemma} + \label{lem:7:ordinalfacts} \begin{enumerate}[(a)] \item $0$ is an ordinal, and if $\alpha$ is an ordinal, so is $\alpha + 1$. @@ -27,7 +28,7 @@ or $\alpha \ni \beta$. \end{enumerate} \end{lemma} -\begin{proof} +\begin{refproof}{lem:7:ordinalfacts} We have already proved (a) before. (b) Fix $x \in \alpha$. Then $x \subseteq \alpha$. @@ -41,12 +42,12 @@ As $\alpha$ is transitive, we have that $z, y, x \in \alpha$. Thus $z \in x \lor z = x \lor z \ni x$. - $z = x$ contradicts Fund: + $z = x$ contradicts \AxFund: Consider $\{x,y\}$. Then $x \cap \{x,y\}$ is non empty, as it contains $y$. Furthermore $x \in y \cap \{x,y\} $ - $z \ni x$ also contradicts Fund: + $z \ni x$ also contradicts \AxFund: If $x \in z$, then $z \ni x \ni y \ni z \ni x \ni \ldots$. $\{x,y,z\}$ yields a contradiction, as $y \in x \cap \{x,y,z\}$, $z \in y \cap \{x,y,z\}$, @@ -58,7 +59,7 @@ (c) Say $\alpha \subsetneq \beta$. Pick $\xi \in \beta \setminus \alpha$ such that $\eta \in \alpha$ for every $\eta \in\xi \cap \beta$. - (This exists by Fund). + (This exists by \AxFund). We want to see that $\xi = \alpha$. We have $\xi \subseteq \alpha$ by the choice of $\xi$. On the other hand $\alpha \subseteq \xi$: @@ -115,13 +116,13 @@ If that is not the case, then $\alpha_0 \in \alpha_0 \cup \beta_0$ and $\beta_0 \in \alpha_0 \cup \beta_0$. - $\alpha_0 \in \alpha_0$ violates Fund. + $\alpha_0 \in \alpha_0$ violates \AxFund. Hence $\alpha_0 \in \beta_0$. By the same argument, $\beta_0 \in \alpha_0$. - But this violates Fund, + But this violates \AxFund, as $\alpha_0 \in \beta_0 \in \alpha_0$. \end{subproof} -\end{proof} +\end{refproof} \begin{lemma} Let $X$ be a set of ordinals, @@ -134,7 +135,7 @@ It is actually the case that $\bigcap X \in X$: Pick $\alpha \in X$ such that $\alpha \subseteq \beta$ for all $\beta \in X$. This exists -by Fund and since all ordinals are comparable. +by \AxFund and since all ordinals are comparable. Then $\alpha = \bigcap X$. \begin{notation} diff --git a/inputs/lecture_08.tex b/inputs/lecture_08.tex index b0e5747..76874fe 100644 --- a/inputs/lecture_08.tex +++ b/inputs/lecture_08.tex @@ -41,8 +41,8 @@ has the following axioms: \forall x .~\exists y .~ y = \bigcup x. \] \end{axiom} -\begin{axiom}[Power] - \yalabel{Powerset Axiom}{(Pow)}{ax:bg:pow} +\begin{axiom}[Power Set] + \yalabel{Power Set Axiom}{(Pow)}{ax:bg:pow} \[ \forall x .~\exists y .~ y = \cP(x). \] @@ -128,7 +128,7 @@ Furthermore $F\,''a \coloneqq \{y : \exists x \in a .~(x,y) \in F\}$. \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 + \AxFund is equivalent to saying that this is a well-founded relation for every $M$. \end{enumerate} \end{example} @@ -136,10 +136,10 @@ Furthermore $F\,''a \coloneqq \{y : \exists x \in a .~(x,y) \in F\}$. \begin{lemma} \label{lem:fundseq} - In $\ZFC - \Fund$, + In $\ZFC - \AxFund$, the following are equivalent: \begin{itemize} - \item \Fund, + \item \AxFund, \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} @@ -149,12 +149,12 @@ Furthermore $F\,''a \coloneqq \{y : \exists x \in a .~(x,y) \in F\}$. 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. + violates \AxFund. For the other direction let $M \neq \emptyset$ be some set. - Suppose that \Fund does not hold for $M$. + Suppose that \AxFund does not hold for $M$. - Using \Choice, + Using \AxC, we construct an infinite sequence $x_0 \ni x_1 \ni x_2 \ni \ldots$ of elements of $M$. @@ -186,7 +186,7 @@ Furthermore $F\,''a \coloneqq \{y : \exists x \in a .~(x,y) \in F\}$. &&~ ~\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 + $G$ exists as it can be obtained by \AxAus from ${}^{< \omega}M$. By induction, for every $n \in \omega$, @@ -224,7 +224,7 @@ Furthermore $F\,''a \coloneqq \{y : \exists x \in a .~(x,y) \in F\}$. \yaref{lem:fundseq}. \end{proof} \begin{remark} - In $\ZF$ this is a weaker form of \Choice. + In $\ZF$ this is a weaker form of \AxC. \end{remark} The construction of $g$ in the previous proof was a special case of diff --git a/logic.sty b/logic.sty index be7a7fa..ec89433 100644 --- a/logic.sty +++ b/logic.sty @@ -114,27 +114,15 @@ \DeclareSimpleMathOperator{OD} \DeclareSimpleMathOperator{AC} \newcommand{\AxC}{\yarefs{ax:c}} -\newcommand{\AxSep}{\yarefs{ax:sep}} % Separation -\newcommand{\Choice}{\yarefs{ax:c}} -% \DeclareSimpleMathOperator{Choice} -% \DeclareSimpleMathOperator{Fund} -\newcommand{\Fund}{\yarefs{ax:fund}} -\DeclareSimpleMathOperator{Pair} -\DeclareSimpleMathOperator{Union} -\DeclareSimpleMathOperator{Rep} +\newcommand{\AxExt}{\yarefs{ax:ext}} % AoE +\newcommand{\AxFund}{\yarefs{ax:fund}} % AoF +\newcommand{\AxPair}{\yarefs{ax:pair}} % AoP +\newcommand{\AxUnion}{\yarefs{ax:union}} % AoU +\newcommand{\AxPow}{\yarefs{ax:pow}} +\newcommand{\AxRep}{\yarefs{ax:rep}} +\newcommand{\AxInf}{\yarefs{ax:inf}} % AoI +\newcommand{\AxAus}{\yarefs{ax:aus}} % Separation -\DeclareSimpleMathOperator{Pow} -\DeclareSimpleMathOperator{AoE} -\DeclareSimpleMathOperator{AoF} -\DeclareSimpleMathOperator{AoP} -\DeclareSimpleMathOperator{AoU} -\DeclareSimpleMathOperator{AoI} -\DeclareSimpleMathOperator{Inf} - - -\renewcommand{\Aus}{\text{Aus}} -% \DeclareSimpleMathOperator{Aus} -\DeclareSimpleMathOperator{Infinity} \DeclareSimpleMathOperator{CH} \DeclareSimpleMathOperator{DC} diff --git a/todo b/todo deleted file mode 100644 index 74e4fe2..0000000 --- a/todo +++ /dev/null @@ -1 +0,0 @@ -Better REF for axioms