• Let $M$ be a countable mode of ZFC (exists by lowenheim skolem).
• Let $\Omega \equiv \{0, 1\}$ ( $\Omega$ for subobject classifier).
• Take $P$ to be the set of partial functions from $\aleph_2 \times \aleph_0 \to \Omega$ with finite support
• Note that elements of $P$ can be thought of as finite lists, where we know the values where they are 0, where they are 1.
• Also note that elements of $P$ can be arranged in an obvious partial order.

§ Ideal of a post

• We define an ideal $I \subseteq P$ to be a set of elements which are pairwise compatible (all pairs of elements have a union), and is downward closed (all elements with less information is present in the ideal).
• More formally, for any $i \in I$ and $p \in P$, if $p \leq i$, then $p \in I$. So $P \leq I \implies P \in I$.
• For every $i, i' \in I$, there is some $j \in I$ such that $i, i' \leq j$ ( $I$ is a directed set).

§ Maximal ideal

• A maximal ideal $I_\star \subseteq P$ is an ideal such that for any $p \in P$, either $p$ is incompatible with $I_\star$, or $p$ is in $I_\star$.

§ Density in a poset

• A subset $D$ of a poset $P$ is dense iff for any $p \in P$, there is some $d \in D$ such that $d \geq p$. Intuitively, at any point in the poset, it is possible to "add more information" to reach $D$.

§ Generic Ideals

• We say that an ideal $G$ is generic iff $G \cap D \neq \emptyset$ for all dense $D \subseteq P$.
• For any countable model $M$, and a poset $P$ over it, We claim that for any $p \in P$, a generic ideal $G_p$ which contains $p$ ( $p \in G$) exists.

§ Proof: Generic ideal always exists

• We wish to find a generic ideal that contains a special $p_\star \in P$.
• Let $D_1, D_2, \dots$ be an enumeration of the dense subsets of $P$ that are members of the countable model $M$.
• We can perform such an enumeration because $M$ is countable, and thus only has countable many sets.
• We will create a new sequence $\{q_i\}$ which hits each $\{D_i\}$.
• Start with $q_0 \equiv p_star$.
• Since $D_1$ is dense, there is some $d_1 \in D_1$ such that $d_1 \geq q_0$. Set $q_1 \equiv d_1$.
• This gives us a sequence $\{q_i\}$.
• Build an ideal $I^\star_p \equiv \{ p \in P : \exists i, p \leq q_i \}$. That is, we build the union of all the lower sets of $q_i$. So this can also be written as $I^\star_p \equiv \cup_i \downarrow q_i$, where $\downarrow(p) \equiv \{ p' : p' \leq p \}$, the down set of $p$.
• $I^\star_p$ is downward closed by construction, and is directed because for any two elements $a, b \in I$, there is some $q_i, q_j$such that $a \in \downarrow q_i$, $b \in downarrow q_j$, and WLOG, if $q_i \leq q_j$, then $a, b \leq q_j$, thereby making the set directed.

§ Separative poset

• $P$ is separative iff $p \leq q \leq p$ implies $p = q$.

§ Generic ideal of separative poset is not in the model

• Claim: if $G$ is a generic ideal of $P \subseteq M$, then $G$ is not in $M$.
• Let $H \subseteq P$, $H \in M$. Consider the set $D_H \equiv \{ p \in P : \exists h \in H, \texttt{incompatible}(p, h) \}$.
• Intuitively, $D_H$ is the set of all elements of $P$ which are incompatible with some element of $H$.
• We must have $D_H$ \in $M$ by comprehension(M), since $M$ is a model of $ZFC$ ahd $D_H$ is a susbet of $P$.
• To see that $D_H$ is dense, for any element $p \in P$, we need to find an element $d \in D$ such that $p \leq d$. See that $d \in D$ iff there exists some $h \in H$, such that incompatible(d, h).
• Since $D_H$ is dense, we have that $G \cap D_H \neq \emptyset$, This gives us some element $g \in G$ such that incompatible(g, p)for some $p \in H \subseteq P$.
• TODO: this makes no sense!

§ Definition of forcing

• An element $p \in P$ forces the sentence $\phi(\vec \tau)$ iff $\phi^{M[G]}(\vec \tau^G)$ is true for every generic ideal $G$ such that $p \in G$. For every formula $\phi$, forcing tells us for which pairs of $p, \vec \tau$ it is the case that $\phi^{M[G]}(\vec \tau^G)$ is true. It is written as $p \Vdash \phi(\vec \tau)$.
• Written differently, we say that $p \in P$ forces $phi(\vec \tau)$, iff for any $G \subseteq P$, $p \in G \implies \phi^G(\vec \tau^G)$ is true.
• That is to say, we can decide the truth of $\phi^G(\vec \tau^G)$ by looking at the presence/absence of $p$ in $G$.
• See that for a fixed $\phi$, forcing gives us a relation $\subseteq P \times M^k$.
• What we want to show is this that this forcing relation, for each $\phi$, is definable in $M$.
• This will show that the collection of $p$ that force a $\phi$ is in $M$ (project the first components of $P \times M^k$.

§ Fundamental theorem of forcing

• For every formula $\phi$, for every generic ideal $G$ over $P$:
• 1. Definability: there is a set $F(\alpha, \phi) \in M$ such that $p \Vdash \phi(\vec \tau)$ ( $p$ forces $\tau$) if and only if $(p, \vec \tau) \in F(\alpha, \phi)$. That is, the forcing relation is definable in $M$
• 2. Completeness: $\phi^{M[G]}(\vec \tau^G)$ is true iff there is a $g \in G$ such that $g \Vdash \phi(\vec \tau)$. That is, any true sentence in $M[G]$ must have a witnessing $p \in G$ which forces it, for any generic ideal $G$.
• 3. Coherence/Stability: If $p \Vdash \phi$, for all $q \geq p$, we have $q \Vdash \phi$. Truth once forced cannot be unforced, truth is inflationary, truth is stable, etc.
• The FTF (fundamental theorem of forcing) is an algorithm on the ZFC syntax. It takes a formula $\phi$, and produces a ZFC proof of (1), (2), (3).

§ Architecture of FTF

• TODO, here I Am!

§ Net to capture generic ideal

• If $G$ is a generic ideal of $P$, and $G \subseteq (Z \in M)$, then there is a $p \in G$, such that all $q$ such that $p \leq q$ are in $Z$. That is, $\forall G, \exists p \in G, \forall q \in G, p \leq q \implies q \in Z$.
• QUESTION: How can $Z \in M$ if $G$ is a proper class relative to $M$, and $G$ is a subset of $M$? Isn't a superset of a proper class a proper class?
• Recalling that (p, q) ∈ P are compatible iff ∃r ∈ P, p ≤ r ∧ q ≤ r. If no such r exists, then (p, q) are incompatible.
• Suppose we take some (p, q) ∈ P. We can have (1) p ≤ q, (2) q ≤ p, (3) (p, r) compatible, (4) (p, r) incompatible. Consider:

a   r \ / \  p   d  e   \ /   |    c----*

• If q=a then p <= q
• If q=c then q <= p.
• If q=d then ∃r, (p <= r, q <= r) compatible.
• If q=e, then (p, e) incompatible.
• We wish to show that there is a $p \in G$ such that all its extensions lie in $Z$.
• That is to say, all of the extensions of $p \in G$ do not lie in $Z^c$.

§ Proof of net lemma

• To prove: If $G$ is a generic ideal of $P$, and $G \subseteq (Z \in M)$, then there is a $p \in G$, such that all $q$ such that $p \leq q$ are in $Z$. That is, $\forall G, \exists p \in G, \forall q \in G, p \leq q \implies q \in Z$.

• Let $D$ be the set of elements in $p$ that is incompatible with every element in $Z^c$: $D \equiv \{ p \in P: \forall q \in Z^c, p \perp q \}$
• If $D$ were dense in $P$, then an element $r \in G \cap D$ would be the element we are looking for, where all the extensions of $r$ is in $G$.
• Let's try to show that $D$ is dense. Let $p \in P$ be arbitrary. We need to find a $d \in D$ such that $p \leq d$.
• If $p \perp q$ for every $q \in Z^c$, then we are done, since $p \in D$, and thus $p \leq p \in D$.
• On the other hand, suppose there is a $q$ such that $p \not \perp p$. That is, there is an $r$such that $p \leq r, q \leq r$.
• Now what? Now we make an observation: See that we can freely add $\uparrow Z^c = \{ r : \exists q \in Z^c, q \leq r \}$into $D$, because (1) if we consider $G \cap (D \cup Z^c)$, then $G \cap Z^c = \emptyset$. (2) $G \cap \uparrow Z^c$ could have an element $\uparrow r \in \uparrow Z^c, \in G$. But this cannot happen, because this means that $\exists q \in Z^c, q \leq \uparrow r$. But since $G$ is downward closed and $r \in G$, this means that $q \in G$, which is a contradiction as $q \in Z^c$ which has empty intersection with $G$.
• TLDR: We can fatten up any set with $Z^c$, while not changing the result of $G \cap -$!
• So we build $D' \equiv D \cup \uparrow Z^c$, which is to say, $D' \equiv \{ (p \in P: \forall q \in Z^c, p \perp q) \} \cup \{ r \in P : (\exists q \in Z^c, q \leq r)\}$.
• We claim that $D'$ is dense. Suppose we have some $p \in P$. (1) $p \perp q$ for all $q \in Z^c$, and thus $p \leq p \in D'$ and we are done. Otherwise, assume that there is some $q$ such that $p \not \perp q$. then there is an $r \in P$, such that $p \leq r, q \leq r$. This gives us an $r \in D'$ such that $p \leq r \in D'$ and we are done.

§ Simpler proof of net lemma (Unverified)

• Let $D \equiv \{ p \in P : \forall q \in Z^c, p \not \leq q \}$.
• Let's now pick a concrete $p \in P$, and try to show that $D$ is dense. so we need to find a $d \in D$ such that $p \leq d$.
• Easy case: If $p$ has no extensions in $Z^c$, then $p \in D$ by defn of $D$; we are done since $p \leq (p \in D)$, ahd thus density is fulfilled.
• Hard case: Suppose $p$ does have an extension $q \in Z^c$, what then? How do I find an element of $d \in D$such that $p \leq d$? ( $d$ for extension)?
• Hard case: See that we will be using $D$ to consider $r \in (G \cap D)$ to find an element $r$ whose every extension lies in $Z$. So suppose we add $q \in Z^c, p \leq q$ into $D$ (ie, $D' \equiv D \cup \{q\}$).
• While $q \in D$, we will still have that $q \not \in G \cap D$, because $q$ lies in $Z^c$, which has zero intersection with $G \subseteq Z$!
• Thus, we can throw $Z^c$ in $D$ "for free" to fatten $D$ up to make it more dense, while knowing that $G$ will cull this $Z^c$ portion.
• So define $D' \equiv \{ p \in P : \forall q \in Z^c, p \not \leq q\} \cup Z^c$
• We claim that $D'$ is dense.
• Suppose $p \in P$. If for all $q \in Z^c$, $p \not \leq q$, then $p \in D'$. Otherwise, suppose $p \leq q \in Z^c$. Then we have $p \leq (q \in Z^c \subseteq D'$. Thus $D'$ is dense.
• Let $r \in G \cap D$. Then we cannot have $r$ come from the portion of $Z^c$, since $G \cap Z^c = \emptyset$. This means that $r$ came from the first part of the set $D'$, where no extension of $p$ lies in $Z^c$. Thus we are done.

§ Intuition for Net definition

• A net $Z \subseteq P$ could be defined in two ways: (A) $\forall p \in P, \exists z \in Z, p \leq Z$, or (B) $\forall z \in Z, \exists p \in P, z \leq p$.
• It can't be (B), because (B) has a trivial solution $Z = \emptyset$!
• It should be (A), because (A) forces $Z$ to be "non-trivial", since I can test it against all $p \in P$.

§ Names and name creation

• Let $N$ (for names) be defined transifinitely, where $N_0 \equiv \emptyset$, $N_{i+1} \equiv \mathcal{P}(P \times N_i) \cap M$, and take the union in the usual way at the limit ordinal.
• Intuitively, names let us create "hypothetical sets", which are realised into real sets for each subset $S \subseteq P$. We keep those elements which are tagged by $s \in S$, and we remove those sets which are not.

§ Forcing equality

§ Step 1: Defining the forcing tuple set $F^{x=y}$.

• to decide equality of $\tau, \tau'$, it is very sensitive to $G$ because elements can appear/disappear based on $G$.
• We want all triplets $(p, \tau, \tau')$ where $\tau, \tau' \in \texttt{NamedSet}(M)$such that $p$ forces $\tau^G = \tau'^G$.
• Recall that $p$ forces $\tau^G = \tau'^G$ means: $\tau^G = \tau'^G$ if and only if $p \in G$.
• Thus, $p$ must be such that it is NECESSARILY POSSIBLY TRUE that every element $\sigma^G \in \tau^G$ must also be such that $\sigma^G \in \tau'^G$, and also vice verss: every $\sigma'^G \in \tau'^G$ must be such that $\sigma'^G \in \tau^G$.
• Let us prove the forward direction, where we want to force $\sigma \in \tau$ implies $\sigma \in tau'$.
• Whenever $q \geq p$, and $(\sigma, q) \in \tau$, there must be an $r \geq q$ such that $(\sigma^G \in \tau')$.
• We might be tempted to say that $r$ implies $(sigma^G \in \tau'^G)$ iff $(\sigma, r) \in \tau'$, but this is too strong. There could be many different collapses that allowed for $\sigma, r \in \tau'$. That is, we could have some $\xi^G \in \tau^G$, and $r$ forces $\xi^G = \sigma^G$.
• Now it looks like we need to define equality in terms of equality. We just perform induction on name rank, because to have $\sigma \in \tau$, the name rank of $\sigma$ must be lower than $\tau$ because we built the name rank universe by induction.
• So we define the condition on tripets $(p, \tau, \tau')$ of name rank less than $\alpha$ to be that for ALL $(\sigma, q) \in tau$ where $q \geq p$, there is $(\xi, r) \in \tau'$ such that $r \geq q$ and $(r, \sigma, \xi) \in F^{x=y}_{max(nr(\sigma), nr(\xi))}$,
• So we define the relation $F^{x=y}$ by name rank induction.

§ Step 2: defining the net

• Next, we need to define the net $Z$.
• Let $Z^{=} \equiv \{ q \in P: \forall (\sigma, q) \in \tau, \exists (\xi, r) \in tau', r \geq q \land (r \models \sigma = \xi)$ \}.
• Question: What is the meaning of the $\models$ symbol in this context?
• SID: I guess $r \models \sigma = \xi$ is syntactic sugar for $(r, \sigma, \xi) \in F^{x=y}$.
• See that $Z^{=}$ is the set of all $q$ for which $\tau$ is possibly a subset or equal to $\tau'$.
• By the inductive hypothesis of name rank, FTF holds for $\sigma, \xi$ and it follows that $Z^{=} \in M$[I have no fucking idea what this means ].

§ Step 4: The equivalence of net, modality, relativized inclusion:

• $\tau^G \subseteq \tau'^G$ implies
• $G \subseteq Z^{=}$ implies
• $\exists p \in G, \forall q \geq p, q \in Z^{=}$ implies
• $\tau^G \subseteq \tau'^G$

Therefore, all these conditions are equivalent.

• We will show that $\tau^G \subseteq \tau'^G$ implies that $G \subseteq Z^{=}$. This by the net lemma will implu that there is a $p \in G$ such that all larger elements will be trapped in the net $Z^{=}$.
• Then we will prove that if there is such a $p \in G$ which traps elements in the net, then we have $\tau^G = \tau'^G$.