Is a name a sheaf?

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.

• "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? Feb 1, 2019 at 7:54
• 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. Feb 1, 2019 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.

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'$$.

• I'm not very familiar with sheaves - ultimately how different is this from what I described? Feb 21, 2019 at 0:30
• 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. Feb 21, 2019 at 0:36
• Great, I thought so, I just wasn't certain. Feb 21, 2019 at 0:37