From 430ad82e8ba03f69f92700ffbbccf8057620e4ba Mon Sep 17 00:00:00 2001
From: Josia Pietsch <git@jrpie.de>
Date: Sun, 5 Nov 2023 00:50:26 +0100
Subject: [PATCH] lecture 04

---
 inputs/lecture_04.tex | 19 ++++++++++---------
 inputs/lecture_05.tex |  2 +-
 logic.sty             |  2 ++
 logic2.tex            |  2 +-
 4 files changed, 14 insertions(+), 11 deletions(-)

diff --git a/inputs/lecture_04.tex b/inputs/lecture_04.tex
index 3bdf433..90ea9e6 100644
--- a/inputs/lecture_04.tex
+++ b/inputs/lecture_04.tex
@@ -93,7 +93,7 @@ $\ZFC$ consists of the following axioms:
     The axiom of infinity says that there exists and inductive set.
 \end{axiom}
 
-\begin{axiomscheme}[Separation]
+\begin{axiomschema}[\vocab{Separation}]
     % TODO :(Aus)
     Let $\phi$ be some fixed
     fist order formula in $\cL_\in$.
@@ -110,7 +110,7 @@ $\ZFC$ consists of the following axioms:
     \[
     \forall a.~\exists b.~(b = \{x \in a; \phi(x)\}).
     \]
-\end{axiomscheme}
+\end{axiomschema}
 
 \begin{notation}
     \todo{$\cap, \setminus, \bigcap$}
@@ -126,21 +126,22 @@ $\ZFC$ consists of the following axioms:
         \item $\forall a.~\exists b.~(b = \bigcap a)$.
     \end{itemize}
 \end{remark}
-\begin{axiomscheme}[\vocab{Replacement} (Fraenkel)]
+\begin{axiomschema}[\vocab{Replacement} (Fraenkel)]
     Let $\phi$ be some $\cL_{\in }$ formula.
     Then
     \[
     \forall v_1 .~\exists  b.~\forall y.~(y \in b \iff \exists  x .~(x \in a \land \phi(x,y,v_1,v_p))).
     \]
-\end{axiomscheme}
+\end{axiomschema}
 
 \begin{axiom}[\vocab{Choice}]
     Every family of non-empty sets has a \vocab{choice set}:
-    \todo{TODO}
-    \[
-    \forall x.~(\forall y \in x.~x \neq \emptyset \land
-    \forall y \in  x \forall y' \in x .(y \neq y' \implies x \cap y' = \emptyset) \implies \exists  z .~\forall y \in x .~\exists  u.~(z \cap y = \{u\})).
-    \]
+    \begin{IEEEeqnarray*}{rCl}
+        \forall x .~&(&\\
+                    && ((\forall y \in x.~y \neq \emptyset) \land (\forall y \in x .~\forall y' \in x .~(y \neq  y' \implies y \cap y' = \emptyset))\\
+                    && \implies\exists  z.~\forall y \in x.~\exists u.~(z \cap y = \{u\})\\
+                    &)&
+    \end{IEEEeqnarray*}
 \end{axiom}
 
 
diff --git a/inputs/lecture_05.tex b/inputs/lecture_05.tex
index dd4db06..6434571 100644
--- a/inputs/lecture_05.tex
+++ b/inputs/lecture_05.tex
@@ -283,7 +283,7 @@
     \end{claim}
     \begin{subproof}
         Suppose that $\dom(r) \subsetneq a$
-        and $\ran(r) \susbsetneq b$.
+        and $\ran(r) \subsetneq b$.
 
         Let $x \coloneqq  \min(a \setminus \dom(r))$
         and $y \coloneqq  \min(b\setminus \ran(r))$.
diff --git a/logic.sty b/logic.sty
index 8b9710c..20f5018 100644
--- a/logic.sty
+++ b/logic.sty
@@ -93,6 +93,8 @@
 \hypersetup{colorlinks, citecolor=violet, urlcolor=blue!80!black, linkcolor=red!50!black, pdfauthor=\@author, pdftitle=\ifdef{\@course}{\@course}{\@title}}
 
 \NewFancyTheorem[thmtools = { style = thmredmargin} , group = { big } ]{warning}
+\NewFancyTheorem[thmtools = { style = thmredmarginandfill} , group = { big } ]{axiom}
+\NewFancyTheorem[thmtools = { style = thmredmarginandfill, name = Axiom Schema} , group = { big } ]{axiomschema}
 
 \DeclareSimpleMathOperator{ran} % TODO: ran vs range
 \DeclareSimpleMathOperator{range} % TODO
diff --git a/logic2.tex b/logic2.tex
index 888ff01..c06909b 100644
--- a/logic2.tex
+++ b/logic2.tex
@@ -27,7 +27,7 @@
 \input{inputs/lecture_01}
 \input{inputs/lecture_02}
 \input{inputs/lecture_03}
-% \input{inputs/lecture_04}
+\input{inputs/lecture_04}
 \input{inputs/lecture_05}