diff --git a/inputs/lecture_19.tex b/inputs/lecture_19.tex
index 8e49054..6eba058 100644
--- a/inputs/lecture_19.tex
+++ b/inputs/lecture_19.tex
@@ -168,7 +168,7 @@ Again by a similar argument we get:
 \section{Forcing}
 Recall that a structure $\bP = (P, \le )$
 is a partially ordered set (\vocab{poset})
-if $\le $ is reflexive, symmetric nd transitive.
+if $\le $ is reflexive, symmetric and transitive.
 
 \begin{definition}
     \label{def:forcingwords}
diff --git a/inputs/lecture_21.tex b/inputs/lecture_21.tex
index e337b5f..f671e44 100644
--- a/inputs/lecture_21.tex
+++ b/inputs/lecture_21.tex
@@ -155,7 +155,4 @@
     to $M$.
 \end{example}
 
-Next steps:
-\begin{itemize}
-    \item Make sense of $M[g]$.
-\end{itemize}
+Next we want to define $M[g]$.
diff --git a/inputs/lecture_22.tex b/inputs/lecture_22.tex
new file mode 100644
index 0000000..12abc76
--- /dev/null
+++ b/inputs/lecture_22.tex
@@ -0,0 +1,254 @@
+\lecture{22}{2024-01-22}{More Forcing}
+
+\begin{warning}+
+    Forcing will not be relevant for the exam.
+    Because of a lack of time, this is more of an outlook
+    than a thorough presentation of the material.
+\end{warning}
+
+For the rest of the section, let us fix
+a transitive model $M$ of $\ZFC$
+a partial order $\mathbb{P}$
+and an  $M$-generic filter $g$.
+
+\begin{definition}[$\mathbb{P}$-names]
+    For an ordinal $\alpha \in M$%
+    \footnote{Recall that $\Ord_M = \Ord \cap M$.},
+    let $M^{\mathbb{P}}_\alpha$,
+    the \vocab{$\mathbb{P}$-names} in $M$ of rank $\le \alpha$,
+    be defined as follows:
+
+    \[
+        \tau \in M_{\alpha}^{\mathbb{P}} :\iff
+        \tau \in M \land
+        \tau \subseteq  \mathbb{P} \times  \bigcup \{M_\beta^{\mathbb{P}}: \beta < \alpha\},
+    \]
+    i.e.~the elements of $\tau \in  M_\alpha^{\mathbb{P}}$
+    are of the form $(p, \sigma)$,
+    where $p \in \cP$ and $\sigma \in M^{\mathbb{P}}_\beta$
+    for some $\beta < \alpha$.
+
+    Finally $M^{\mathbb{P}} = \bigcup \{M_\alpha^{\mathbb{P}} : \alpha \in M\}$.
+\end{definition}
+
+Let $R$ be the relation on $M^{\mathbb{P}}$ defined by
+$\sigma R \tau$ iff $\exists  p \in \mathbb{P}.~(p,\sigma) \in \tau$.
+If $\tau \in M^\mathbb{P}$
+and $(p, \sigma) \in \tau$,
+then $\sigma \in \{p, \sigma\} \in (p,\sigma) \in \tau$,
+so the relation $R$
+is well founded.
+\begin{definition}
+    Let $\tau \in M_\alpha^{\mathbb{P}}$.
+    Then $\tau^g$,
+    the \vocab{$g$-interpretation of $\tau$},
+    is defined to be
+    \[
+    \{\sigma^g : \exists  p \in g .~(p,\sigma) \in \tau\}.
+    \]
+\end{definition}
+
+\begin{definition}
+    $M[g]$,
+    the forcing extension of $M$
+    given by  $g$,
+    is
+    \[
+    \{ \tau^g : \tau \in M^{\mathbb{P}}\} .
+    \]
+\end{definition}
+\begin{lemma}
+    $M[g]$ is transitive.
+\end{lemma}
+\begin{proof}
+    Trivial!
+\end{proof}
+\begin{lemma}
+    $M \cup \{g\} \subseteq  M[g]$.
+\end{lemma}
+\begin{proof}
+    For all $x \in M$ we need to find a name \vocab{$\check{x}$}
+    such that $\check{x}^g = x$.
+
+    We can recursively (along $\in$) define
+    \[
+    \check{x} = \{(p, \check{y}) : p \in \mathbb{P} \land y \in x\}.
+    \]
+    By induction, $\check{x} \in M$ for all $x \in M$.
+    \begin{claim}
+        $\check{x}^g = x$.
+    \end{claim}
+    \begin{subproof}
+        Recall that $\mathbb{P} \neq \emptyset$.
+        Inductively, we get
+        \begin{IEEEeqnarray*}{rCl}
+            \check{x}^g &=& \{\check{y}^g : \exists  p \in  g.~(p,\check{y}) \in \check{x}\}\\
+                        &\overset{\text{induction}}{=}& \{y : \exists  p \in  g.~(p,\check{y}) \in \check{x}\}\\
+                        &\overset{\text{definition of $\check{x}$}}{=}& \{y : y \in x\} = x.
+        \end{IEEEeqnarray*}
+    \end{subproof}
+
+    So $M \subseteq M[g]$.
+
+
+    We also need a name for $g$.
+    Let \vocab{$\dot{g}$}$ \coloneqq  \{(p, \check{p}) : p \in \mathbb{P}\}$.
+
+    Indeed
+    \begin{IEEEeqnarray*}{rCl}
+        \dot{g}^g &=& \{\check{p}^g : \exists p \in g.~(p, \check{p}) \in \dot{g}\}\\
+                  &=& \{p : p \in g\} = g.
+    \end{IEEEeqnarray*}
+\end{proof}
+
+
+\begin{lemma}
+    \label{lem:mgmodelexfundinfpairunion}
+    $M[g] \models \AxExt, \AxFund, \AxInf, \AxPair, \AxUnion$.
+\end{lemma}
+\begin{proof}
+    \begin{itemize}
+        \item \AxExt:
+
+            The formula $\forall x.~\forall y .~((\forall  z \in x.~z \in y \land \forall z \in y.~z \in x) \to  x = y)$
+            is $\Pi_1$, hence it is true in $M[g]$
+            by %TODO REF downward absolutenes.
+        \item \AxFund:
+            Again,
+             \[
+            \forall x.~(\exists  y \in x .~y = y \to  \exists  y \in x.~\forall z \in y.~z \not\in x)
+            \]
+            is $\Pi_1$.
+        \item \AxInf
+            can be written as
+            \[
+            \exists x .~(\underbrace{\neq  \in x \land \forall  y \in x.y \cup \{y\}  \in x}_{\Sigma_0}).
+            \]
+            We have $ \omega \in M \subseteq M[g]$,
+            so $M[g] \models \AxInf$.
+        \item \AxPair:
+            Let us assume $x,y \in M[g]$,
+            say $x = \tau^g$ and $y = \sigma^g$.
+            Let  $\pi = \{(p,\tau) : p \in \mathbb{P} \} \cup \{(p,\sigma) : p \in \mathbb{P}\} \in M^{\mathbb{P}}$.
+            Then $\pi^g = \{\tau^g, \sigma^g\} = \{x,y\}$,
+            so $\{x,y\} \in M[g]$.
+            As a $\cL_\in$-statement,
+            $z = \{x,y\}$ is $\Sigma_0$,
+            so $M[g] \models \text{``$\{x,y\}$ is the pair of $x$ and $y$''}$.
+            Hence $M[g] \models \AxPair$.
+        \item \AxUnion:
+            Similar to \AxPair.\todo{Exercise}
+    \end{itemize}
+\end{proof}
+
+Still missing are
+\begin{itemize}
+    \item \AxPow,
+    \item \AxAus,
+    \item \AxRep,
+    \item \AxC.
+\end{itemize}
+
+\begin{definition}[\vocab{Forcing relation}]
+    Let $M$ be a countable transitive model of $\ZFC$
+    and let $\mathbb{P} \in M$ be a partial order.
+    Let $p \in \mathbb{P}$
+    and let $\phi$ be a $\cL_{\in }$-formula.
+
+    Let $\tau_1,\ldots, \tau_k \in M^{\mathbb{P}}$ be names.
+
+    We say that
+    $p$ \vocab[force]{forces}  $\phi(\tau_1,\ldots, \tau_k)$,
+    \[
+        p  \Vdash^{\mathbb{\cP}}_{M} \phi(\tau_1, \ldots, \tau_k),
+    \]
+    if for all $h \subseteq \mathbb{P}$
+    which are $\mathbb{P}$-generic over $M$
+    with $p \in h$,
+    \[
+    M[h] \models\phi(\tau_1^h, \ldots, \tau_k^h).
+    \]
+\end{definition}
+\begin{theorem}
+    Fix an $\cL_\in$-formula $\phi$.
+    Then the relation
+    \[
+        R = \{(p,\tau_1,\ldots,\tau_k : p  \Vdash ^{\mathbb{P}}_M \phi(\tau_1,\ldots,\tau_k)\}
+    \]
+    is definable over $M$
+    (in the parameter $\mathbb{P}$).
+\end{theorem}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{theorem}[\vocab{Forcing Theorem}]
+    Let $M$,  $\mathbb{P}$, $g$,
+    be as above,
+    let $\phi$ be a formula,
+    and let $\tau_1, \ldots, \tau_k \in M^{\mathbb{P}}$.
+    Then the following are equivalent:
+    \begin{enumerate}[(1)]
+        \item $M[g] \models \phi(\tau_1^g, \ldots, \tau_k^g)$.
+        \item There is some $p \in g$ with
+            \[
+            p  \Vdash^{\mathbb{P}}_M \phi(\tau_1,\ldots, \tau_k).
+            \]
+            
+    \end{enumerate}
+\end{theorem}
+\begin{proof}
+    Omitted.
+\end{proof}
+
+\begin{theorem}
+    $M[g] \models \ZFC$.
+\end{theorem}
+\begin{proof}
+    We have already shown a part of this in
+    \yaref{lem:mgmodelexfundinfpairunion}.
+
+    Let us show that $M[g] \models \AxAus$,
+    the rest is similar and left as an exercise.%
+    \footnote{or done next semester in Logic IV!}
+
+    Let $\phi$ be a formula,
+    let $a, x_1,\ldots,x_k \in M[g]$.
+    We need to see
+    \[M[g] \models \exists y.~y = \{z  \in a : \phi(z, x_1,\ldots,x_k)\}.\]
+
+    If suffices to show that there is some $y \in M[g]$
+    with $y = \{ z \in a : M[g] \models \phi(z, x_1,\ldots,x_k)\}$.
+
+    For this, let us construct a name for  $y$.
+    Let $a = \tau^g$, $x_i = \sigma_i^g$.
+
+    Let
+    \[
+    \pi = \{(p,\rho) : \exists \overline{p} > p.~(\overline{p}, \rho) \in \tau \land
+    p  \Vdash^{\mathbb{P}}_M \phi(\rho, \sigma_1, \ldots, \sigma_k)\}.
+    \]
+
+    We have $\pi \in M$, since the relation
+    $ \Vdash^{\mathbb{P}}_M$ can be defined in $M$.
+
+    Let $z \in a$ such that $M[g] \models \phi(z, x_1,\ldots,x_n)$.
+    We have $z = \rho^g$
+    for some  $\rho$
+    and there is  $\overline{p} \in g$ with $(\overline{p}, \rho) \in \pi$.
+    Now $M[g] = \phi(\rho^g, \sigma_1^g,\ldots\sigma_k^g)$.
+
+    Let $p'  \Vdash^{\mathbb{P}}_M \phi(\rho, \sigma_1,\ldots, \sigma_k)$,
+    where $p' \in g$.
+    We have $p', \overline{p} \in g$,
+    so there is some $p \le  p', \overline{p}$ with $p \in g$.
+    Then $(p,\rho) \in \pi$,
+    so $\rho^g \in \pi^g$.
+
+    This shows that
+    \[
+    \{z \in a : M[g] \models \phi(z,x_1,\ldots,x_k)\}  \subseteq \pi^g.
+    \]
+    The other inclusion is easy.
+
+\end{proof}
diff --git a/logic2.tex b/logic2.tex
index 4686286..12b278c 100644
--- a/logic2.tex
+++ b/logic2.tex
@@ -45,6 +45,7 @@
 \input{inputs/lecture_19}
 \input{inputs/lecture_20}
 \input{inputs/lecture_21}
+\input{inputs/lecture_22}
 
 
 \cleardoublepage