Merge branch 'master' of https://git.abstractnonsen.se/josia-notes/w23-logic-2

.gitea/workflows/build.yaml

@@ -12,7 +12,7 @@ jobs:
       - name: Prepare pages
         run: |
             mkdir public
-            mv build/logic2.pdf build/logic2.log README.md public
+            mv build/*.pdf build/*.log README.md public
       - name: Deploy to pages
         uses: actions/pages@v1
         with:

inputs/lecture_01.tex

@@ -109,6 +109,7 @@
     If $A \sim B$, there is a bijection $h\colon A \to B$.
 \end{theorem}
 \begin{proof}
+    \gist{%
     Let $f\colon A \hookrightarrow B$ and $g\colon B \hookrightarrow A$
     be injective.
     We need to define a bijection $h\colon A \to  B$.
@@ -146,6 +147,7 @@
     It is clear that this is bijective.
 
     \todo{missing picture $f(A^{\text{odd}}) \subseteq B^{\text{even}}$, $f(A^\infty) = B^\infty$}.
+}{Preimage sequence}
 \end{proof}
 
 \begin{definition}

inputs/lecture_02.tex

@@ -1,4 +1,5 @@
 \lecture{02}{2023-10-19}{Topology on $\R$}
+\gist{%
 \begin{definition}
     A set $O \subseteq \R$ is called \vocab{open} in $\R$ iff it is the union
     of a set of open intervals.
@@ -20,6 +21,7 @@
 \begin{remark}+
     $\{O \subseteq \R\} \sim 2^{\aleph_0} < \cP(\R)$.
 \end{remark}
+}{}
 
 \begin{definition}
     We call $x \in \R$
@@ -28,9 +30,11 @@
     there is some $y \in A$, $y \in (a,b)$, $y \neq x$.
     We write \vocab{$A'$} for the set of all accumulation points of $A$.
 \end{definition}
+\gist{%
 \begin{example}
     $\{\frac{1}{n+1} | n \in \N\}' = \{0\}$.
 \end{example}
+}{}
 
 \begin{lemma}
     \label{lem:closedaccumulation}
@@ -38,9 +42,11 @@
 \end{lemma}
 \begin{refproof}{lem:closedaccumulation}
     ``$\implies$''
+    \gist{%
     Let $A$ be closed. Suppose that $x \in A' \setminus A$.
     Then there exists $(a,b) \ni x$
     disjoint from $A$. Hence $x \not\in A' \lightning$
+    }{trivial.}
 
     ``$\impliedby$''
     Suppose $A' \subseteq  A$.
@@ -48,6 +54,7 @@
         $A \subseteq  \R$ is closed iff all Cauchy sequences
         in $A$ converge in $A$.
     \end{claim}
+    \gist{%
     \begin{subproof}
         Let $A$ be closed and $\langle x_n : n \in \omega \rangle$
         a Cauchy sequence in $A$.
@@ -62,6 +69,7 @@
         we may pick $x_n \in (x - \frac{1}{n+1}, x + \frac{1}{n+1}) \cap A$
         for all $n < \omega$.
     \end{subproof}
+    }{}
 
     Now if $A' \subseteq  A$ and $A$ were not closed,
     there would be some Cauchy-sequence $(x_n)$
@@ -92,6 +100,7 @@ We want to prove two things:
     Then $P \sim \R$.
 \end{lemma}
 \begin{proof}
+\gist{%
     It suffices to find an injection $f\colon \R \hookrightarrow P$.
     We have $\underbrace{\{0,1\}^{\omega}}_{\text{infinite 0-1-sequences}} \sim \R$,
     hence it suffices to construct $f\colon \{0,1\}^\omega\hookrightarrow P$.
@@ -132,4 +141,5 @@ We want to prove two things:
     and $f(t') \in [a_{t'\defon{n}}, b_{t'\defon{n}}]$
     which are disjoint.
     Thus $f(t) \neq f(t')$, i.e.~$f$ is injective.
+}{Cantor scheme.}
 \end{proof}

inputs/lecture_03.tex

@@ -77,7 +77,7 @@ all condensation points are accumulation points.
     \begin{subproof}
         $P \neq \emptyset$: $\checkmark$ 
 
-        $P \subseteq  P'$ (i.e. $P$ is closed):
+        $P \subseteq  P'$:
         % \begin{IEEEeqnarray*}{rCl}
         %     P &=& \{x \in A | \text{every open neighbourhood of $x$ is uncountable}\}\\
         %     &\subseteq & \{x \in A | \text{every open neighbourhood of $x$ is at least countable}\} = P'.
@@ -97,7 +97,7 @@ all condensation points are accumulation points.
         But then $(a,b) \cap A$ is at most countable
         contradicting $ x \in P$.
 
-        $P' \subseteq P$ :
+        $P' \subseteq P$ (i.e.~$P$ is closed):
         Let $x \in P'$.
         Then for $a < x < b$ the set
         $(a,b) \cap P$
@@ -111,7 +111,7 @@ all condensation points are accumulation points.
     \] 
 \end{refproof}
 
-\todo{Alternative proof of Cantor-Bendixson}
+\gist{\todo{Alternative proof of Cantor-Bendixson}}{}
 % \begin{remark}
 %     There is an alternative proof of Cantor-Bendixson, going as follows:
 %     Fix $A \subseteq  \R$ closed.

inputs/lecture_04.tex

@@ -5,13 +5,14 @@
 \section{\texorpdfstring{$\ZFC$}{ZFC}}
 
 % 1900, Russel's paradox
-\todo{Russel's Paradox}
+% \todo{Russel's Paradox}
 $\ZFC$ stands for
 \begin{itemize}
     \item \textsc{Zermelo}’s axioms (1905), % crises around 19000
     \item \textsc{Fraenkel}'s axioms,
     \item the \yaref{ax:c}.
 \end{itemize}
+\gist{
 \begin{notation}
     We write $x \subseteq y$ as a shorthand
     for $\forall z.~(z \in x \implies z \in y)$.
@@ -45,6 +46,7 @@ $\ZFC$ stands for
         \forall u.~((u \in z) \iff (u \in x \land u \not\in y)).
     \]
 \end{notation}
+}{Trivial, boring notation.}
 $\ZFC$ consists of the following axioms:
 \begin{axiom}[\vocab{Extensionality}]
     \yalabel{Axiom of Extensionality}{(Ext)}{ax:ext} % (AoE)
@@ -148,13 +150,15 @@ $\ZFC$ consists of the following axioms:
 \begin{axiomschema}[\vocab{Replacement} (Fraenkel)]
     \yalabel{Axiom of Replacement}{(Rep)}{ax:rep}
     Let $\phi$ be some $\cL_{\in }$ formula
-    with free variables $x, y$.\todo{Allow more variables}
+    with free variables $x, y$.
     Then
-    \[
+    \begin{IEEEeqnarray*}{l}
-        \forall x \in a.~\exists !y \phi(x,y) \implies \exists b.~\forall x \in a.~\exists y \in b.~\phi(x,y).
+        \forall v_1 \ldots \forall v_p.~\\
+        \left[\left( \forall x \exists! y.~\phi(x,y,\overline{v})\right) \to \forall a .~\exists b .~\forall y.~(y \in b \leftrightarrow \exists x (x \in a \land \phi(x,y, \overline{v}))\right]
+    \end{IEEEeqnarray*}
+        %\forall x \in a.~\exists !y \phi(x,y) \implies \exists b.~\forall x \in a.~\exists y \in b.~\phi(x,y).
         % \forall v_1 \ldots \forall v_p .~\forall x.~ \exists y'.~\forall y.~(y = y' \iff \phi(x))
         % \implies \forall a.~\exists b.~\forall y.~(y \in b \iff \exists x.~(x \in a \land \phi(x))
-    \]
 \end{axiomschema}
 
 \begin{axiom}[\vocab{Choice}]

inputs/lecture_05.tex

@@ -23,6 +23,7 @@
     \]
 \end{definition}
 
+\gist{%
 \begin{definition}
     For sets $x, y$ we write
     $(x,y)$ for $\{\{x\}, \{x,y\}\}$.
@@ -108,7 +109,7 @@
 \end{definition}
 
 \begin{fact}
-    Given sets $d, b$ then
+   Given sets $d, b$ then
     $\leftindex^d b$ exists.
 \end{fact}
 \begin{proof}
@@ -130,7 +131,7 @@
    (In other mathematical fields, this is sometimes
    denoted as $f(a)$. We don't do that here.)
 \end{notation}
-
+}{[Some boring definitions omitted.]}
 \begin{definition}
     A binary relation $\le $ on a set $a$
     is a \vocab{partial order}
@@ -168,7 +169,6 @@
     x \in b \land \forall y \in b.~y \le x.
     \]
 
-
     In a similar way we define \vocab[Minimal element]{minimal elements} 
     and the \vocab{minimum} of $b$.
     We say that $x $ is an \vocab{upper bound} 
@@ -181,6 +181,7 @@
     (This does not necessarily exist.)
     Similarly $\text{\vocab{$\inf$}}(b)$ is defined.
 \end{definition}
+\gist{
 \begin{remark}+
     Note that in a partial order,
     a maximal element is not necessarily a maximum.
@@ -200,6 +201,7 @@
     We write $(a,\le_a) \cong (b, \le_b)$
     if they are isomorphic.
 \end{definition}
+}{}
 \begin{definition}
     Let $(a,\le)$ be a partial order.
     Then $(a,\le)$ is 

inputs/lecture_06.tex

@@ -8,6 +8,7 @@
     Then $a$ has a maximal element.
 \end{theorem}
 \begin{refproof}{thm:zorn}
+    \gist{%
     Fix $(a, \le )$ as in the hypothesis.
     Let $A \coloneqq  \{ \{(b,x) : x \in b\}  : b \subseteq a, b \neq \emptyset\}$.
     Note that $A$ is a set (use separation on  $\cP(\cP(a) \times  \bigcup \cP(a))$).
@@ -65,6 +66,36 @@
     Then $B = B_{u_0}^{\le^{\ast\ast}}$.
     So $\le^{\ast\ast} \in W$, but now $u_0 \in b$.
     So $b$ must have a maximum.
+    \todo{Why does this prove the lemma?}
+}{
+    \begin{itemize}
+        \item $A  \coloneqq  \{\{(b,x) : x \in b\}, b \subseteq a, b \neq \emptyset\}$.
+        \item \AxC $\leadsto$ choice function on $A$,
+            $f\colon  \cP(a) \setminus \{\emptyset\}  \to  a$, $f(b) \in b$.
+        \item $\le^\ast$ on $a$:
+            \begin{itemize}
+            \item $W \coloneqq  \{\le' \text{wo on} b \subseteq a : \forall u,b \in b.~u \le' v \implies u \le v, B_u^{\le '} \neq \emptyset, u = f(B^{\le '}_u)\}$ where
+                \item $B_u^{\le'} = \{w \in  a : w \text{ $\le $-upper bound of } \{v \in  b : v <' u\} \}$.
+            \end{itemize}
+        \item $\le', \le '' \in W \implies \le' \substack{\subseteq\\\supseteq} \le''$:
+            \begin{itemize}
+                \item $(b, \le') \overset{g}{\cong} (c, \le'') (\defon{v})$.
+                \item $g = \id_b$:
+                    \begin{itemize}
+                        \item $u_0$ $\le'$ minimal with $g(u_0) \neq u_0$.
+                        \item $\{w \in b : w <' u_0\} \overset{g \defon{\ldots}}{=} \{w \in c : w <'' g(u_0)\}$.
+                        \item $B^{\le '}_{u_0}  = B_{g(u_0)}^{\le ''} \neq \emptyset$,
+                        so $u_0 = f(B^{\le '}_{u_0}) = f(B^{\le ''}_{g(u_0)}) = g(u_0) \lightning$
+                    \end{itemize}
+            \end{itemize}
+        \item  $\le^\ast \coloneqq  \bigcup W$ is wo on $b \subseteq a$.
+        \item Suppose $b$ has no maximum. Then  $B \cap b = \emptyset$.
+        \item $u_0 \coloneqq f(B)$, $\le^{\ast\ast} = \le^\ast \cup \{(u,u_0) | u \in b\}  \cup \{(u_0,u_0)\}$.
+        \item $B = B_{u_0}^{\le^{\ast\ast}}$, so $\le^{\ast\ast} \in W$,
+            but $u_0 \in b \lightning$. ?
+    \end{itemize}
+}
+
 \end{refproof}
 
 \begin{remark}
@@ -82,6 +113,7 @@
     Then $A$ contains a $\subseteq$-maximal element.
 \end{corollary}
 
+\gist{%
 \begin{remark}[Cultural enrichment]
     Other assertions which are equivalent
     to the \yaref{ax:c}:
@@ -96,12 +128,14 @@
         \item Every set can be well-ordered.%\footnote{This is clearly false.}
     \end{itemize}
 \end{remark}
+}{}
 % \begin{remark}
 %     The axiom of choice is true.
 % \end{remark}
 
 \pagebreak
 \subsection{The Ordinals}
+\gist{
 \begin{goal}
     We want to define nice representatives of the equivalence classes
     of well-orders.
@@ -115,7 +149,7 @@ We can hence form the smallest inductive set
 Note that $\omega$ exists, as it is a subset of the inductive
 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\}$.
@@ -147,16 +181,19 @@ We have the following principle of induction:
     and for all $y, z \in x$,
     we have that $y = z$, $y \in z$ or $y \ni z$.
 \end{definition}
+\gist{
 Clearly, the $\in$-relation is a well-order on an ordinal $x$.
 \begin{remark}
     This definition is due to \textsc{John von Neumann}.
 \end{remark}
+}{}
 
 \begin{lemma}
     Each natural number (i.e.~element of $\omega$)
     is an ordinal.
 \end{lemma}
 \begin{proof}
+\gist{
     We use \yaref{lem:induction}.
     Clearly $\emptyset$ is an ordinal.
     Now let $\alpha$ be an ordinal.
@@ -169,6 +206,7 @@ Clearly, the $\in$-relation is a well-order on an ordinal $x$.
     since $\alpha$ is an ordinal.
     Suppose $x = \alpha$.
     Then either $y = x$ or $y \in \alpha = x$.
+}{Induction}
 \end{proof}
 
 \begin{lemma}

inputs/lecture_07.tex

@@ -20,6 +20,7 @@
     \end{enumerate}
 \end{lemma}
 \begin{refproof}{lem:7:ordinalfacts}
+\gist{
     We have already proved (a) before.
 
     (b) Fix $x \in \alpha$. Then $x \subseteq \alpha$.
@@ -113,6 +114,7 @@
         But this violates \AxFund,
         as $\alpha_0 \in  \beta_0 \in \alpha_0$.
     \end{subproof}
+}{Long and tedious, but not many ideas.}
 \end{refproof}
 
 \begin{lemma}
@@ -146,6 +148,7 @@ for example $\bigcup \omega = \omega$.
     Otherwise $\alpha$ is called
     a \vocab[Ordinal!limit]{limit ordinal}.
 \end{definition}
+\gist{
 \begin{observe}
     Note that $\alpha$ is a limit ordinal iff for all
     $\beta \in \alpha$, $\beta + 1 \in \alpha$:
@@ -158,7 +161,8 @@ for example $\bigcup \omega = \omega$.
     then by definition there is some $\beta \in \alpha$,
     with $\beta + 1 = \alpha$, so $\beta + 1 \not\in \alpha$.
 \end{observe}
-
+}{}
+\gist{
 \begin{notation}
     If $\alpha, \beta$ are ordinals,
     we write $\alpha < \beta$ for $\alpha \in \beta$
@@ -185,3 +189,4 @@ for example $\bigcup \omega = \omega$.
         \item $\omega +1 = \omega \cup \{\omega\} , \omega + 2, \ldots$,
     \end{itemize}
 \end{example}
+}{}

inputs/lecture_08.tex

@@ -1,6 +1,7 @@
 \lecture{08}{2023-11-13}{Induction and recursion}
 
 \subsection{Classes}
+\gist{
 It is often very handy to work in a class theory rather than
 in set theory.
 
@@ -11,10 +12,11 @@ sets (denoted by lower case letters)
 and classes (denoted by capital letters),
 as well as one binary relation symbol $\in$
 for membership.
+}{}
 
 \vocab{Bernays-Gödel class theory} (\vocab{BG})
 has the following axioms:
-
+\gist{
 \begin{axiom}[Extensionality]
     \yalabel{Axiom of Extensionality}{(Ext)}{ax:bg:ext}
     \[
@@ -54,6 +56,7 @@ has the following axioms:
     \exists x .~(\emptyset \in x \land \left( \forall y \in x .~y \cup \{y\}  \in x \right)).
     \]
 \end{axiom}
+}{\AxExt, \AxFund, \AxPair, \AxUnion, \AxPow, \AxInf as from $\ZF$.}
 
 Together with the following axioms for classes:
 
@@ -108,10 +111,10 @@ Furthermore $F\,''a \coloneqq  \{y : \exists  x \in  a .~(x,y) \in F\}$.
 \end{axiom}
 
 
-\todo{notation: $\emptyset, \cap$}
+\gist{\todo{notation: $\emptyset, \cap$}}{}
 
 
-\todo{the following was actually done in lecture 9}
+\gist{(The following was actually done in lecture 9, but has been moved here for clarity.)}{}
 
 $\BGC$ (in German often NBG\footnote{\vocab{Neumann-Bernays-Gödel}})
 is defined to be  $\BG$

inputs/lecture_11.tex

@@ -75,7 +75,7 @@ We often write $\kappa, \lambda, \ldots$ for cardinals.
     \end{itemize}
 }
 \end{proof}
-We may now use the \yaref{lem:recursion}
+We may now use the \yaref{thm:recursion}
 to define a sequence $\langle \aleph_\alpha : \alpha \in \OR \rangle$
 with the following properties:
 \begin{IEEEeqnarray*}{rCl}

inputs/lecture_14.tex

@@ -322,7 +322,7 @@ We have shown (assuming \AxC to choose contained clubs):
             and $S_1 \coloneqq \{\xi < \kappa : \cf(\xi) = \omega_1\}$.
             Clearly these are disjoint.
             They are both stationary:
-            Let $c \subseteq \kappa$ be a club.
+            Let $C \subseteq \kappa$ be a club.
             Let $(\xi_i : i \le \omega_1)$
             be defined as follows:
             $\xi_0 \coloneqq  \min C$,

inputs/lecture_15.tex

@@ -60,7 +60,7 @@
 Recall the following:
 
 \begin{definition}
-    A substructure $X \subseteq  V_\theta$\todo{make this more general. Explain why $V_\theta$ is a model}
+    A substructure $X \subseteq  V_\theta$\gist{\todo{make this more general. Explain why $V_\theta$ is a model}}{}
     is an \vocab{elementary substructure}
     of $V_\theta$,
     denoted $X \prec V_{\theta}$,\footnote{more formally $(X,\in ) \prec (V_{\theta})$}

inputs/lecture_17.tex

@@ -236,8 +236,7 @@ We will only proof
         \item $X \le Y :\iff \{\alpha < \omega_1 : f_X(\alpha) \le f_Y(\alpha)\}$ stationary.
         \item (2) $X\le Y \lor Y \le X$:
             Suppose $X \not\le Y, Y \not\le X$. Choose witnessing clubs $C, D$.
-            $C \cap D$ is club, but then $f_X(\alpha) \le f_Y(\alpha)$ or
+            $C \cap D$ is club, so $C\cap D \ni \alpha \implies f_X(\alpha) \substack{\nleq\\\ngeq} f_Y(\alpha) \lightning$
-            $f_X(\alpha) \ge f_Y(\alpha)$ for $\alpha \in C \cap D$.
         \item (3) $X \subseteq \aleph_{ \omega_1}$, then $|\underbrace{\{Y \subseteq \aleph_{ \omega_1} : Y \le X\}}_{A}| \le \aleph_{ \omega_1}$
             \begin{itemize}
                 \item Suppose $|A| \ge \aleph_{ \omega_1 + 1}$.
@@ -245,9 +244,21 @@ We will only proof
                     $2^{\aleph_1} = \aleph_2 \implies$ at most $\aleph_2$ such $S_Y$.
                 \item If $\forall  S \in \cP( \omega_1).~ |\underbrace{\{Y \in A : S_Y = S\}}_{A_S}| < \aleph_{ \omega_1 + 1}$,
                     then $|A| \le \aleph_2 \cdot  <\aleph_{ \omega_1 + 1}$ $\lightning$  $\aleph_{ \omega_1 + 1}$ regular.
-                \item So $\exists S \in \omega_1.~|A_S| = \aleph_{ \omega_1 + 1 + 1}$.
+                \item So $\exists S \in \omega_1.~|A_S| = \aleph_{ \omega_1 + 1}$.
-                    % TODO TODO TODO hier weiter!
+                \item Fix surjection $\langle g_\alpha : \aleph_\alpha \twoheadrightarrow f_X(\alpha) + 1 : \alpha \in S \rangle$.
+                    ($f_Y(\alpha) \le f_X(\alpha) < \aleph_{\alpha+1}$)
+                \item $\forall  Y \in A_S$ define $\overline{f}_Y \colon  S \to  \aleph_{ \omega_1}, \alpha \mapsto \min \{\xi : g_\alpha(\xi) = f_Y(\alpha)\}$.
+                \item $S^\ast$ ($S \cap$ limit ordinals) is stationary.
+                \item $\forall Y \in A$ define $h_Y\colon S^\ast \to  \omega_1, \alpha \mapsto \min \{\beta < \alpha : \overline{f}_Y(\alpha) < \aleph_\beta\}$.
+                \item Apply \yaref{thm:fodor} to $h_Y, S^\ast$ to get $T_Y \subseteq S^\ast$ stationary with $h_Y\defon{T_Y}$ constant.
+                \item $\exists T.~|\underbrace{\{Y \in A_S : T_Y = T\}}_{A_{S,T}}| = \aleph_{ \omega_1 + 1}$.
+                \item Let $\{\beta\}  = h_Y''T$, i.e.~$\overline{f}_Y(\alpha) < \aleph_{\beta}$ for $Y\in A_{S,T}, \alpha \in T$.
+                \item $\leftindex^T \aleph_\beta \le 2^{\aleph_\beta \cdot \aleph_1} = \aleph_{\beta+1} \aleph_2 < \aleph_{ \omega_1}$.
+                \item $\exists \tilde{f}\colon T \to \aleph_\beta .~ |\underbrace{\{Y \in A_{S,T} : \overline{f}_Y\defon{T} = \tilde{f}\} }_{A_{S,T,\tilde{f}}}| = \aleph_{ \omega_1 + 1}$.
+                \item $Y,Y' \in A_{S,T,\tilde{f}} \implies \forall \alpha \in T.~f_Y(\alpha) = f_{Y'}\left( \alpha \right) \overset{T \text{ unbounded}}{\implies} Y = Y'$
+                    Thus $|A_{S,T, \tilde{f}} | \le 1 \lightning$.
             \end{itemize}
+
         \item Define sequence $\langle X_i : i < \aleph_{ \omega_1 + 1} \rangle$
             of subsets of $\aleph_{\omega_1}$:
             \begin{itemize}
@@ -259,7 +270,7 @@ We will only proof
                 \item $P \coloneqq \{Y \subseteq \aleph_{ \omega_1} : \exists  i < \aleph_{ \omega_1 + 1}.~Y \le X_i\}$
             \end{itemize}
         \item $|P| \overset{\text{in fact } =}{\le} \aleph_{ \omega_1 + 1} \aleph_{ \omega_1} = \aleph_{ \omega_1 + 1}$ by (3).
-        \item $X \in \cP(\aleph_{ \omega_1}) \setminus M \implies \forall i < \aleph_{ \omega_1 + 1}.~X_i \le X$
+        \item $X \in \cP(\aleph_{ \omega_1}) \setminus P \implies \forall i < \aleph_{ \omega_1 + 1}.~X_i \le X$
             $\lightning$ (3).
             Thus $P = \cP(\aleph_{ \omega_1})$.
     \end{itemize}

inputs/lecture_18.tex

@@ -77,6 +77,7 @@
     \end{enumerate}
 \end{theorem}
 \begin{proof}
+\gist{%
     2. $\implies$ 1.:
     Fix $j\colon  V \to M$.
     Let $U = \{X \subseteq  \kappa : \kappa \in j(X)\}$.
@@ -221,11 +222,60 @@ such that
 as otherwise $\forall \delta < \alpha. ~  \kappa \setminus X_\delta \in U$,
 i.e.~$\emptyset = (\bigcap_{\delta < \alpha} \kappa \setminus X_{\delta}) \cap X \in U \lightning$.
 We get $[f] = [c_{\delta}]$,
-so $\beta = \sigma([f]) = \delta([c_{\delta}]) = j(\delta) = \delta$,
+so $\beta = \sigma([f]) = \sigma([c_{\delta}]) = j(\delta) = \delta$,
 where for the last equality we have applied the induction hypothesis.
 So $j(\alpha) \le \alpha$.
 
+For all $\eta < \kappa$, we have $\eta = \sigma([c_{\eta}]) < \sigma([c_{\id}]) < \sigma([c_{\kappa}])$,
+so $j(\kappa) > \kappa$.
+
 % It is also easy to show $j(\kappa) > \kappa$.
+}{%
+    $2 \implies 1$:
+    Fix $j\colon  V \to M$. $U \coloneqq  \{X \subseteq  \kappa : \kappa \in j(X)\}$ is an UF:
+    \begin{itemize}
+        \item $M \models j(X \cap Y) = j(X) \cap j(Y)$,
+            hence $\kappa \in j(X) \cap j(Y) \implies \kappa \in j(X \cap Y)$
+        \item $M \ni X \subseteq Y \implies  Y \in M$, $\emptyset \not\in M$ (same argument)
+        \item $\kappa \in U$:
+            \begin{itemize}
+                \item $\forall \alpha \in \OR.~ j(\alpha) \in \Ord, j(\alpha) \ge \alpha$:
+                    \begin{itemize}
+                        \item Write $\alpha\in \OR$ and use $\alpha \in \OR \iff M \models j(\alpha) \in \OR$.
+                        \item Suppose $j(\alpha) < \alpha$, $\alpha$ minimal,
+                            but $M \models j(j(\alpha)) < j(\alpha) \implies j(j(\alpha)) < j(\alpha)$.
+                    \end{itemize}
+                \item $j(\kappa) \neq \kappa \implies j(\kappa) > \kappa \implies \kappa \in j(\kappa)$.
+            \end{itemize}
+        \item Ultrafilter: $\kappa \in j(\kappa) = j(X \cup (\kappa \setminus X)) = j(X) \cup j(\kappa \setminus X)$.
+        \item $< \kappa$ closed: For $\theta < \kappa$, $X_i \in U$:
+            $\kappa \in \bigcap_{i < \theta} j(X_i) = j\left( \bigcap_{i < \theta} X_i \right) \in U$.
+            ($j(\theta) = \theta$, so $j\left( \langle X_i : i < \theta \rangle \right) = \langle j(X_i) : i < \theta \rangle$.
+        \item Not principal:
+            $\xi < \kappa \implies j(\{\xi\}) = \{\xi\} \not\ni \kappa$.
+    \end{itemize}
+    $1 \implies 2$:
+    \begin{itemize}
+        \item Fix $U$. Consider $\leftindex^\kappa V$.
+        \item $f \sim g :\iff \{\xi < \kappa: f(\xi) = g(\xi)\} \in U$.
+        \item $[f] \coloneqq \{g : g \sim f \land g \in V_\alpha \text{ for minimal } \alpha\}$ (Scott's Trick).
+        \item $[f] \tilde{\in } [g] :\iff \{\xi < \kappa: f(\xi ) \in g(\xi)\}  \in U$.
+        \item \yaref{thm:los}: $(\cF, \tilde{\in }) \models \phi([f_1], \ldots, [f_k]) \iff \{\xi < \kappa: (V, \in ) \models \phi(f_1(\xi), \ldots, f_k(\xi))\} \in U$.
+        \item $\overline{j}(x) \coloneqq  [ \xi \mapsto x]$.
+        \item $\tilde{\in }$ well-founded: lift decreasing sequences ($U$ is $<\kappa$ closed, $ \omega < \kappa$)
+        \item $\tilde{\in }$ set-like $\overset{\yaref{thm:mostowksi}}{\leadsto}$ $(\cF, \tilde{\in }) \overset{\sigma}{\cong} (M, \in )$.
+        \item $j \coloneqq  \sigma \circ \overline{j}$.
+        \item $\alpha < \kappa \implies j(\alpha) = \alpha$ (know $j(\alpha) \ge \alpha$):
+            \begin{itemize}
+                \item Induction for $j(\alpha) \le \alpha$: Fix $\alpha$, $\sigma([f]) = \beta \in j(\alpha)$.
+                \item $[f] \tilde{\in }[c_\alpha]$.
+                \item $\exists  \delta < \alpha.~[f] = [c_\delta]$ ($U $ is $<\kappa$ closed)
+                \item $\beta = \sigma([f]) = \sigma([c_\delta]) = j(\delta) \overset{\text{IH}}{=} \delta \in \alpha$.
+            \end{itemize}
+        \item $j(\kappa) \neq \kappa$:
+            $\forall \eta < \kappa.~\eta = \sigma([c_{\eta}]) < \sigma([\id]) < \sigma([\kappa])$.
+    \end{itemize}
+}
 \end{proof}
 
 \begin{theorem}[\L o\'s]

inputs/lecture_22.tex

@@ -137,7 +137,7 @@ is well founded.
             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}
+            Similar to \AxPair.\gist{\todo{Exercise}}{}
     \end{itemize}
 \end{proof}