What is the precise relationship between forcing on a poset and the topos of double-negation sheaves on this poset?

Question

I've seen various statements that the Boolean-valued models of ZFC occurring in model-theoretic forcing are "really" the topos of sheaves on an appropriate site, but never a fully precise statement. What exactly is the relationship, and where can I find this written down in a clear, simple way?

More precisely, let $\mathbb{P}$ be a poset and $B$ its completion to a Boolean algebra. Then, the machinery of forcing gives a Boolean-valued model of ZFC (let's ignore issues related to the universe, countable transitive models, etc. unless they really become crucial) $V^{(B)}$ such that the truth values of the axioms of ZFC are $1$, and the forcing relation can be defined as $p \Vdash \phi$ for $p \in B$ iff the truth value of $\phi$ is at least $p$.

On the other hand, we may consider $\mathbb{P}$ as a site with the double negation topology (for some $p \in \mathbb{P}$, a collection $S$ of elements $s \in \mathbb{P}$, $s \leq p$ covers $p$ iff for all $q \leq p$ there is some $s \in S$ with $s \leq q$; i.e. $S$ is "dense" below $p$) and take the Boolean topos $\mathscr{V}_\mathbb{P}$ of sheaves on this site. The subsheaves of the terminal object in this topos form a Boolean algebra $\Omega$, and we can assign elements of $\Omega$ as "truth values" of sentences $\phi$ via the Kripke-Joyal semantics. This lets us define a "forcing relation" for $p \in \Omega$ as $p \Vdash' \phi$ iff the terminal map from the Yoneda image of $p$ factors through the truth value of $\phi$.

What is the exact relationship between $V^{(B)}$ and $\mathscr{V}_\mathbb{P}$? In what sense is $\mathscr{V}_\mathbb{P}$ a model of ZFC? (i.e. can it be used directly to prove consistency results in the same way that $V^{(B)}$ can?) I would like to say something like "$p \Vdash \phi$ iff $p \Vdash' \phi$", but strictly speaking this doesn't quite make sense since the formulas are expressed in two slightly different languages (i.e. the language for Kripke-Joyal semantics is that of type theory).

I would love to see this written down in detail somewhere.

(As far as I can tell, a generic filter is not strictly relevant to this question; however, I would be curious if it has an interesting interpretation on the sheaf side).

Answer 1

One good way of seeing the connection is given in Section 4 of Michael Fourman’s paper Sheaf models for set theory (JPAA, Vol 19, 1980).

For any Grothendieck topos $\newcommand{\E}{\mathcal{E}}\E$, there’s a canonical ‘cumulative hierarchy’ in $\E$, i.e. a sequence of objects $V^\E_\alpha$, for $\alpha \in \mathrm{On}$, given by taking power-objects at successor stages and colimits at limit stages, so in particular $V^\E_0 = 0$. Moreover, these carry membership relations $(\in_\alpha) \rightarrowtail V^\E_\alpha \times V^\E_\alpha$; and the total sequence can be seen as a model of IZF, and when the topos is Boolean, a model of ZF. (There are several ways to deal with the fact that it’s a sequence of objects not a single object of $\E$ — I won’t go into that here. Edit: OK, I will — see below!)

Now, when the topos is $\newcommand{\P}{\mathbb{P}} \newcommand{\Sh}{\mathrm{Sh}}\Sh(\P)$, this model $V^{\Sh(\P)}$ ‘is’ the standard Boolean model over $\P$ in several senses. The simplest is Theorem 4.1 in Fourman’s paper. For any sentence $\varphi$ in the language of set theory, we can interpret it either in $V^{\Sh(\P)}$ or in the set-theorist’s Boolean-valued model $V\P$, and either way we get an element of $B(\P)$; then Theorem 4.1 says that these interpretations are the same.

A slightly stronger statement, fairly straightforward to prove, is as follows. (Indeed, I can’t see how to prove Fourman’s Thm 4.1 without going via something like this statement.) There’s a (class) bijection between (the colimit over $\alpha$ of) global sections of the objects $V^{\Sh(\P)}_\alpha$, and $\P$-names in the set-theorist’s sense modulo forcing-equality. Then for any formula $\varphi(x_1, \ldots, x_n)$, and $\P$-names $a_1,\ldots,a_n$, and $p \in \P$, we have $p \Vdash \varphi(a_1,\ldots,a_n)$ in the set-theorist’s sense exactly if $(a_1,\ldots,a_n)\mathord{\upharpoonright_p} \in [\![\, \vec x \,|\, \varphi(\vec x)\, ]\!](p) \subseteq V^{\Sh(\P)}(p)$.

A crucial point in proving this is that the sheaves $V^{\Sh(\P)}$ are flabby, so any local section can be extended to a global section. This is why the set-theoretic presentation of the model can get away with only using $\P$-names, i.e. global sections, even though in general the sheaf-theoretic interpretation of quantification ranges over all elements of a sheaf.

---

Regarding the interpretation of logic in the sequence $V_\alpha$:

The simplest approach is to assume an inaccessible cardinal $\kappa$ larger than $\P$, and cut off at $\kappa$ on both the topos-theoretic and set-theoretic sides. So the model on the topos-theoretic side is just $(V_\kappa,\in_\kappa)$, and the interpretation of (I)ZF in it is the standard interpretation of first-order logic in a structure in a topos using the Kripke–Joyal semantics. On the set-theoretic side, one then correspondingly restricts the Boolean-valued model to “hereditarily $\kappa$-small $\P$-names”, i.e. $V\P \cap H_\kappa$.

Then there’s Fourman’s approach, which is to work with the full sequence $V_\alpha$ for $\alpha \in \mathrm{On}$, and define the interpretation of logic in it by hand, in a way which clearly follows the normal Kripke-Joyal semantics except that its quantifications quantify over the whole sequence.

Finally, the modern viewpoint on Fourman’s interpretation is the categories of classes setting, developed for Algebraic Set Theory. One can embed the topos $\E$ into a super-large category of classes $\E'$, whose objects are to the objects of $\E$ what classes are to sets in (I)ZF. In general, $\E'$ can be taken to be a category of ideals on $\E$; when $\E$ is a topos of sheaves on a small site, $\E$ can be taken to be a topos of “large sheaves” on the same site. Either way, $\E'$ is a Heyting category, so one can interpret first-order logic in it, and under the “large sheaves” presentation of $\E'$, this interpretation looks exactly the usual Kripke–Joyal semantics of a topos. And then in $\E'$, we can take the colimit of the sequence $(V_\alpha,\in_\alpha)$, and use that as our model.