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

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).

• You should read this paper of Mike shulman : arxiv.org/abs/1004.3802 The two are not the same and the topos theoretic version does not directly produce a model of ZFC. Model of ZFC are what Mike called material set theory in the title of the paper and topos are what he called structural set theory. There exists procedures (explain in the paper) to go from one to the other that allow to move from consistency results proved in one type of set theory to consistency result proved in the other. – Simon Henry May 16 '17 at 10:17
• Another place to look is MacLane and Moerdijk "Sheaves in Geometry and Logic", section VI.2.6 where this is explained. I'll bet the elephant knows about it too. – Andrej Bauer May 16 '17 at 12:08
• Andre Scedrov and I wrote this up in considerable detail in Chapter 3 of "Freyd's models for the independence of the axiom of choice" [Memoirs of the A.M.S. 79, number 404 (1989)]. – Andreas Blass May 16 '17 at 13:54
• @AndrejBauer: Mac Lane and Moerdijk and the Elephant really don’t explain this connection at all. They both give the topos-theoretic version, and show how to get consistency results from it — but they never discuss the connection with any of the set-theoretic approaches, beyond pointing out that there’s clearly something very analogous going on. – Peter LeFanu Lumsdaine May 16 '17 at 14:44
• Yes, they say that it is essentially the same construction, but do not dive into a technical comparison, that's true. – Andrej Bauer May 16 '17 at 16:07

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!)


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.

• Thanks for the reference. The paper addresses the questions I had in mind, but for the sake of completeness, would you mind clarifying what it means to interpret a formula in the language of set theory in $V^{\mathrm{Sh}(\mathbb{P})}$, and what this has to do with the Kripke-Joyal semantics of the topos? – dorebell May 17 '17 at 6:48
• @dorebell: OK, I’ve clarified that! Hope it helps :-) – Peter LeFanu Lumsdaine May 18 '17 at 10:43