Is a name a sheaf?

Question

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.

Answer 1

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.

Answer 2

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