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}