Forcing in sheaf models of set theory - where do the "generics" disappear to?

Question

I am studying "Sheaves in Geometry and Logic" by Mac Lane & Moerdijk.

In their construction of a topos satisfying $\lnot CH$ they work entirely in the Grothendieck topos of double negation sheaves over the forcing poset. Only at the very end do they point out that one can choose an arbitrary ultrafilter on the Boolean algebra of regular opens, by a simple application of Zorn's lemma; and quotient out by this ultrafilter to return a "two-valued" model.

They note that generic filters are not present in their construction.

My intuition struggles with this.

• If $\mathbb{P}$ is our forcing poset (Say, separative), and $B$ is the lattice of regular opens of $\mathbb{P}$, and $\iota : \mathbb{P} \to B$ is the usual inclusion map, then for $\mathcal{U}$ an arbitrary ultrafilter on $B$, $\iota^{-1}(\mathcal{U})$ may not contain any element of a regular open $A \subset \mathbb{P}$ even though $A \in \mathcal{U}$. Since the forcing translation interprets statements as regular opens, then a sentence may be "true in the model $M[G]$" or $V[G]$ even without any $p$ that forces $\varphi$ to be true. This destroys the "Truth Lemma" in Kunen's set theory book, which says that every sentence which is true in $M[G]$ is forced by some $p \in G$, which is a central part of the forcing argument.
• Even working in the category of sheaves over $\mathbb{P}$ with respect to the double negation topology, if $A$ is a sheaf in the double negation topology over $\mathbb{P}$, and $G$ is a generic filter, then if we define $A_G$ to be the "localization of $A$ at the point $G$" i.e. the colimit of $A$ restricted to $G$, then it's an easy induction argument that a formula of basic first order logic with equality, with parameters from $A_G$, is true iff it is forced by some $p$ in $G$ and some representatives of the germ parameters from $A_G$. (Here I am using forcing in the sense of the Kripke Joyal semantics.) But this induction argument depends in an essential way on the assumption that the filter is generic.
• If $V^B$ is a boolean valued model of set theory, then quotienting out by an arbitrary ultrafilter might result in sentences $\exists x \varphi(x)$ that are deemed valid even though for no set $a$ is the formula $\varphi(a)$ valid. Genericity rescues us here.

Everywhere you look in standard forcing arguments, the assumption of genericity is playing some role. It makes it difficult for me to understand the correspondence between the two proof techniques and establish a translation between them. How, then, intuitively, does Mac Lane get away with saying "choose an arbitrary ultrafilter by Zorn's lemma and quotient out by it" without mentioning genericity once?

Answer 1

Suppose $\mathbb{P}$ is a forcing poset, and we first consider the topos of presheaves on $\mathbb{P}$. Then define $G(p) := \{ q \in \mathbb{P} \mid p \le q \}$ with restriction maps being the obvious inclusions. This defines an object of the topos which is a subobject of the constant presheaf $\mathbb{P}$, or equivalently a global section of $P(\mathbb{P})$, such that $p \Vdash q \in G$ if and only if $p \le q$.

Within this topos model, we also have that $G$ is a filter of $\mathbb{P}$. Furthermore, in this model, $G$ is not not generic: namely, if $D$ is a dense subtype of $\mathbb{P}$ in the base type theory, then for any $p \in \mathbb{P}$, there is some $q \le p$ with $q \in D$, so $q \Vdash q \in G \cap D$. Thus, every $p \not\Vdash G \cap D = \emptyset$, which implies $\Vdash G \cap D \ne \emptyset$ (in the sense of the negation of $G \cap D = \emptyset$, not in the constructive sense of $\exists x, x \in G \cap D$).

Thus, once we pass to the topos of sheaves with respect to the double negation topology, then in that model of type theory, the sheafification of $G$ forms an object satisfying that $G^+$ is a generic filter of the constant sheaf $\mathbb{P}$. So, $G^+$ can stand in where $G$ appears in usual set forcing arguments; for example, if $\mathbb{P}$ is the Cohen forcing poset of functions from a finite subset of $\mathbb{N} \times S$ to $\{ 0, 1 \}$ where $S$ is a type of large enough cardinality, then the usual argument starts with $\bigcup G^+ : \mathbb{N} \times S \to \{ 0, 1 \}$ and uses genericity of $G^+$ to show that this is an entire function with the corresponding function $S \to P(\mathbb{N})$ being injective, etc.