better ref for axioms

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 .~&(&\\

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}

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}

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}

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

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}

todo

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