The technique of forcing, in set theory, can be expressed in topos theory as a form of reasoning about sheaves on the notion of forcing, $\mathbb{P}$, equipped with a "double negation" Grothendieck topology.

In classical presentations of forcing - in Kunen, or Jech, etc. - the objects in the hypothetical universe $M[G]$ or $V[G]$ are "names" - sets which are hereditarily tagged by elements of the forcing poset. The sentences which receive Boolean-valued truth values, or that are able to be forced by an element $p$ of the poset $\mathbb{P}$, are ultimately sentences in the "forcing language" which reason about these names.

It seems likely that there is a direct translation from names in the forcing language to double-negation sheaves over $\mathbb{P}$; but I am having trouble working out the correct recursive definition. Can someone point me towards the translation? It is not spelled out in Mac Lane & Moerdijk.

  • $\begingroup$ "It seems likely that there is a direct translation from names in the forcing language to double-negation sheaves"? Wouldn't the more appropriate translation consider the structure/theory of their partial interpretations in various model fragments? $\endgroup$ – Not Mike Feb 1 at 7:54
  • 1
    $\begingroup$ Have you looked into other works of forcing from a topos theoretic point of view? I know David Roberts wrote about class forcing. It might be explained in his work. $\endgroup$ – Asaf Karagila Feb 1 at 12:42

This is really just a comment, but is way too long. Since in my opinion it's in fact extremely far from an actual answer, I've made it community wiki - I don't think a reputation bonus for it would be appropriate. EDIT: apparently I don't know how to do that (my recollection is that there used to be a cw checkbox, but I don't see it now) - if someone does know how to make this cw, please do.

Here's one way to assign a sheaf to a name which captures the entire structure of the name.

First, the intuitive version. When $\nu$ is a name and $p$ is a condition, we get a class $Elt^*_\nu(p)$ of names given by $$Elt^*_\nu(p)=\{\mu: p\Vdash \mu\in\nu\}$$ (where the set-brackets are used a tad abusively).

This assignment is "sheafy" in the following sense. Put the order topology on $\mathbb{P}$, so that basic open sets are those of the form $$\mathbb{P}_p:=\{q\in\mathbb{P}: q\le p\}$$ for $p\in\mathbb{P}$. Then $p\mapsto Elt^*_\nu(p)$ literally is a sheaf valued in, well, okay fine it's not a sheaf since it's valued in classes, but meh. In particular, restriction = inclusion.

  • A couple minor remarks:

    • We can make things even nicer by replacing $\mathbb{P}$ formally with its finite completion: $\mathbb{P}^+_{pre}$ is the preorder with underlying set consisting of all finite $F\subseteq\mathbb{P}$ admitting a common extension, ordered by $F_0\le F_1$ iff every condition extending every condition in $F_0$ also extends every condition in $F_1$. We then let $\mathbb{P}^+$ be the induced partial order (although forcing with preorders is also perfectly fine). This makes no substantive difference, but does make things a little easier to write on occasion.

    • We could also use instead the standard topology on the set of maximal $\mathbb{P}$-filters, but I think that's a bit further away from the Grothendieck topology idea, since the Grothendieck topology lives on $\mathbb{P}$ itself.

So that's the idea. Now we need to fix it. Luckily, this isn't hard (hence the "meh"):

For names $\nu,\mu$ there is a name $\hat{\mu}$ such that $(i)$ the rank of $\hat{\mu}$ (thought of as a normal set) is less than that of $\nu$ and $(ii)$ for every condition $q$ forcing $\mu\in\nu$ we also have $q\Vdash \mu=\hat{\mu}$.

This means we can safely restrict attention to a small class - in particular, a set - of names and preserve the idea above. Specifically we define the right map $Elt_\nu$ as $$Elt_\nu(p)=\{\mu\in V_{rk(\nu)}: p\Vdash\mu\in\nu\}.$$ This is now genuinely a sheaf, valued in names. Moreover, we can recover $\nu$ up to $\mathbb{1}$-forced equivalence from $Elt_\nu(p)$, so in a precise sense names are sheaves on $\mathbb{P}$ valued in names - an unsurprisingly recursive notion.

It's now worth noting that the construction above satisfies a certain universality property. Namely, fixing a forcing notion $\mathbb{P}$, call a class $\mathcal{C}$ of set-valued sheaves on $\mathbb{P}$ a nameslike class if (playing a bit fast and loose with proper classes - if you want, we're working in NBG or MK instead of vanilla ZFC):

  • Every element of the image of a sheaf $S\in\mathcal{C}$ is a subclass (and necessarily a set) of $\mathcal{C}$.

  • There is a class function $\rho:\mathcal{C}\rightarrow Ord$ or $S\in\mathcal{C}$ and $R\in im(S)$ we have $\rho(R)<\rho(S)$ (this essentially ensures both well-foundedness and set-likeness).

    • OK fine, this is materially redundant (no function can have an element in its image of higher rank than itself), but it's spiritualy non-redundant: the more general picture is to consider an arbitrary class relation $R\subseteq \mathbb{P}\times V^2$ satisfying certain properties, with $R(p,a,b)$ being interpreted as $p\Vdash a\in b$. In principle, the appropriate structures $V[G]_R$ (see below) could be ill-founded, or well-founded yet "taller" than $V$ itself. This seems potentially interesting to me, but unnecessarily general right now, so I want to make it clear that we're ruling it out.

Given any nameslike class $\mathcal{C}$ and any $G$ which is $\mathbb{P}$-generic over $V$, we get a class-sized $\in$-structure $V[G]_\mathcal{C}$ given by essentially taking the extensional collapse of the structure generated by setting $S_0\in S_1$ whenever $S_0\in S_1(p)$ for some $p\in G$. The point now is:

In a precise and strong sense, $V[G]_\mathcal{C}$ always is a sub-thing of $V[G]_{V^\mathbb{P}}$ (= $V[G]$ in the usual sense).

Formalizing and proving this is not hard (although it is a bit tedious).

That's all very classical, and while I've never seen it explicitly I'm sure it's folklore; the next step would be to lift it to the categorial context. The key points should be:

  • Every Grothendieck topology $\tau$ on $\mathbb{P}$ gives rise naturally to an association to each name $\nu$ of a sheaf $Elt_\nu^\tau$ on $(\mathbb{P},\tau)$ valued in (lower-rank) names.

  • Taking $\tau$ to be the double negation topology, we get the construction above (or something equivalent to it).

  • An analogue of the universality property above should hold.

At a glance, it seems this idea will still work, but I'm not familiar enough with the topic to say more about it.


Suppose we have a name $\sigma$; then we can define a corresponding presheaf on $\mathbb{P}$ as $\sigma^{psh} := \amalg_{(p, \tau) \in \sigma, p \in \mathbb{P}} p^{psh}$, where $p^{psh}$ is the presheaf generated by a single element at $p$; i.e. $p^{psh}(q) = \{ 0 \}$ if $q \le p$ and $p(q) = \emptyset$ otherwise. In other words, $\sigma^{psh}$ is the universal presheaf with a generator at level $p$ for every $(p, \tau) \in \sigma$, and $\sigma^{psh}(p) \simeq \{ (q, \tau) \mid (q, \tau) \in \sigma, q \in \mathbb{P}, p \le q \}$. (The presheaf $p^{psh}$ appears frequently as the object of the presheaf topos representing the functor $\Gamma(p, -)$ of taking sections at $p$. In case of a small category $C$ instead of a poset $\mathbb{P}$, the corresponding presheaf would be $p^{psh}(q) = \operatorname{Hom}_C(q, p)$ - though I won't really mention this case in the rest of the exposition.)

If we now take the sheafification of $\sigma^{psh}$, this will intuitively generate the type of elements of $\sigma$. However, there is one more thing to take care of: in order to have extensionality in the resulting model, we will need to take the quotient by the equivalence relation generated by the requirement that $(p, \tau) \sim (p', \tau')$ at level $q\le p, p'$ in the sheaf whenever $q \Vdash \tau = \tau'$ (using the traditional forcing of equality definition).

Now, suppose by abuse of notation we name the resulting quotient sheaf $\sigma$ also. Then for example, we can define an element relation ${\in}_\sigma : \sigma \times \sigma \to \Omega$ by taking the sheafification of the presheaf relation $\sigma^{psh} \times \sigma^{psh} \to \Omega^{psh}, (\tau, \tau') \mapsto (p \mapsto (p \Vdash \tau \in \tau'))$.

Moreover, for any name $\tau$ and $p\in \mathbb{P}$ such that $p \Vdash \tau \in \sigma$, we can construct a corresponding section of $\Gamma(p, \sigma)$ in a straightforward way. This construction will also be compatible with restrictions $q \le p$, and with ${\in}_\sigma$ and equality on $\sigma$, e.g. if $p \Vdash \tau \in \sigma$ and $p \Vdash \tau' \in \sigma$, then ${\in}_{\sigma}(\tau, \tau') = \top_p$ if and only if $p \Vdash \tau \in \tau'$, and $\tau = \tau'$ as sections at $p$ if and only if $p \Vdash \tau = \tau'$. Similarly, for any names $\sigma, \sigma'$ and $p \in \mathbb{P}$ such that $p \Vdash \sigma \subseteq \sigma'$, we can define a monomorphism $\sigma \times p \to \sigma' \times p$ in the slice category over $p$, which again becomes compatible with the construction of sections corresponding to forced elements of $\sigma$ resp. $\sigma'$ above.

TL/DR: For a name $\sigma$, the corresponding sheaf is the universal sheaf with a generator at level $p$ for each $(p, \tau) \in \sigma$ (which we will also call $(p, \tau)$), and with relations $(p, \tau) = (p', \tau')$ at level $q \le p, p'$ whenever $q \Vdash \tau = \tau'$.

  • $\begingroup$ I'm not very familiar with sheaves - ultimately how different is this from what I described? $\endgroup$ – Noah Schweber Feb 21 at 0:30
  • $\begingroup$ My construction of a section of $\Gamma(p, \sigma)$ corresponding to $\tau$ such that $p \Vdash \tau \in \sigma$ should pretty much give that our constructions end up with the same objects. My construction just gives essentially a small presentation of the sheaf. $\endgroup$ – Daniel Schepler Feb 21 at 0:36
  • $\begingroup$ Great, I thought so, I just wasn't certain. $\endgroup$ – Noah Schweber Feb 21 at 0:37

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.