diff --git a/inputs/lecture_04.tex b/inputs/lecture_04.tex
new file mode 100644
index 0000000..3bdf433
--- /dev/null
+++ b/inputs/lecture_04.tex
@@ -0,0 +1,147 @@
+\lecture{04}{}{ZFC}
+
+% Model-theoretic concepts and ultraproducts
+
+\section{$\ZFC$}
+
+% 1900, Russel's paradox
+Russel's Paradox:
+$\ZFC$ stands for
+\begin{itemize}
+    \item \textsc{Zermelo}’s axioms (1905), % crises around 19000
+    \item \vocab{Fraenkel}'s axioms,
+    \item the axiom of choice.
+\end{itemize}
+\begin{notation}
+    We write $x \subseteq y$ as a shorthand
+    for $\forall z.~(z \in x \implies z \in y)$.
+
+    We write $x = \emptyset$ for $\lnot \exists  y . y \in x$
+    and $x \cap y = \emptyset$ for $\lnot \exists  z . ~(z \in x \land z \in y)$.
+
+    We use $x = \{y,z\}$
+    for
+    \[
+    y \in x \land z \in x \land \forall a .~(a \in x \implies a = y \lor a = z).
+    \]
+
+    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}]
+    \[
+    \forall x.~\forall y.~(x = y \iff \forall z.~(z \in x \iff z \in y)).
+    \]
+    Equivalent statements using $\subseteq$:
+    \[
+        \forall x.~\forall y.~(x = y \iff (x \subseteq y \land y \subseteq x)).
+    \]
+\end{axiom}
+
+\begin{axiom}[\vocab{Foundation}]
+    Every set has an $\in$-minimal member:
+    \[
+    \forall  x .~ \left(\exists  a .~(a\in x) \implies
+    \exists  y .~ y \in x \land \lnot \exists z.~(z \in  y \land z \in x)\right).
+    \]
+    Shorter:
+    \[
+    \forall x.~(x \neq \emptyset \implies \exists  y \in x .~ x \cap y = \emptyset).
+    \]
+\end{axiom}
+\begin{axiom}[\vocab{Pairing}]
+    \[
+    \forall x .~\forall y.~ \exists z.~(z = \{x,y\}).
+    \]
+\end{axiom}
+\begin{remark}
+    Together with the axiom of pairing,
+    the axiom of foundation implies
+    that there can not be a set $x$ such that
+    $x \in x$:
+    Suppose that $x \in x$.
+    Then $x$ is the only element of $\{x\}$,
+    but $x \cap \{x\} \neq \emptyset$.
+
+    A similar argument shows that chains like
+    $x_0 \in x_1 \in  x_2 \in x_0$
+    are ruled out as well.
+\end{remark}
+
+\begin{axiom}[\vocab{Union}]
+    \[
+    \forall x.~\exists y.~(y = \bigcup x).
+    \]
+\end{axiom}
+
+\begin{axiom}[\vocab{Powerset}]
+    We write $x = \cP(y)$
+    for
+    $\forall  z.~(z \in x \iff x \subseteq z)$.
+    The powerset axiom (PWA) states
+    \[
+    \forall x.~\exists y.~y=\cP(x).
+    \]
+\end{axiom}
+\begin{axiom}[\vocab{Infinity}]
+    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{axiomscheme}[Separation]
+    % TODO :(Aus)
+    Let $\phi$ be some fixed
+    fist order formula in $\cL_\in$.
+    Then $\text{(Aus)}_{\phi}$
+    states
+    \[
+    \forall v_1 .~\forall v_p .~\forall a .~\exists  b .~\forall x.~
+    (x \in b \implies x \in a \land \phi(x,v_1,v_p))
+    \]
+
+    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
+    \[
+    \forall a.~\exists b.~(b = \{x \in a; \phi(x)\}).
+    \]
+\end{axiomscheme}
+
+\begin{notation}
+    \todo{$\cap, \setminus, \bigcap$}
+    % We write $z = x \cap y$ for $\forall u.~((u \in z) \implies u \in x \land u \in y)$,
+    % $Z = x \setminus y$ for ...
+    % $x = \bigcap y$ for ...
+\end{notation}
+\begin{remark}
+    (Aus) 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)$,
+        \item $\forall a.~\exists b.~(b = \bigcap a)$.
+    \end{itemize}
+\end{remark}
+\begin{axiomscheme}[\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}
+
+\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\})).
+    \]
+\end{axiom}
+
+
+% TODO Hier weiter