Sheaf-theoretic approach to forcing

Question

Inspired by the question here, I have been trying to understand the sheaf-theoretic approach to forcing, as in MacLane–Moerdijk's book "Sheaves in geometry and logic", Chapter VI.

A general comment is that sheaf-theoretic methods do not a priori produce "material set theories". Here "material set theory" refers to set theory axiomatized on the element-of relation $\in$, as usually done, in ZFC. Rather, they produce "structural set theories", where "structural set theory" refers to set theory axiomatized on sets and morphisms between them, as in the elementary theory of the category of sets ETCS. I will always add a collection (equivalently, replacement) axiom to ETCS; let's denote it ETCSR for brevity. Then Shulman in Comparing material and structural set theories shows that the theories ZFC and ETCSR are "equivalent" (see Corollary 9.5) in the sense that one can go back and forth between models of these theories. From ZFC to ETCSR, one simply takes the category of sets; in the converse direction, one builds the sets of ZFC in terms of well-founded extensional trees (modeling the "element-of" relation) labeled by (structural) sets.

So for this question, I will work in the setting of structural set theory throughout.

There are different ways to formulate the data required to build a forcing extension. One economic way is to start with an extremally disconnected profinite set $S$, and a point $s\in S$. (The partially ordered set is then given by the open and closed subsets of $S$, ordered by inclusion.) One can endow the category of open and closed subsets $U\subset S$ with the "double-negation topology", where a cover is given by a family $\{U_i\subset U\}_i$ such that $\bigcup_i U_i\subset U$ is dense. Let $\mathrm{Sh}_{\neg\neg}(S)$ denote the category of sheaves on the poset of open and closed subsets of $S$ with respect to this topology.

Then $\mathrm{Sh}_{\neg\neg}(S)$ is a boolean (Grothendieck) topos satisfying the axiom of choice, but it is not yet a model of ETCSR. But with our choice of $s\in S$, we can form the ($2$-categorical) colimit $$\varinjlim_{U\ni s} \mathrm{Sh}_{\neg\neg}(U)$$ called the filter-quotient construction by MacLane–Moerdijk. I'm highly tempted to believe that this is a model of ETCSR — something like this seems to be suggested by the discussions of forcing in terms of sheaf theory — but have not checked it. (See my answer here for a sketch that it is well-pointed. Edit: I see that well-pointedness is also Exercise 7 of Chapter VI in MacLane–Moerdijk.)

Questions:

1. Is it true that $\varinjlim_{U\ni s} \mathrm{Sh}_{\neg\neg}(U)$ is a model of ETCSR?
2. If the answer to 1) is Yes, how does this relate to forcing?

Note that in usual presentations of forcing, if one wants to actually build a new model of ZFC, one has to first choose a countable base model $M$. This does not seem to be necessary here, but maybe this is just a sign that all of this does not really work this way.

Here is another confusion, again on the premise that the answer to 1) is Yes (so probably premature). An example of an extremally disconnected profinite set $S$ is the Stone-Cech compactification of a discrete set $S_0$. In that case, forcing is not supposed to produce new models. On the other hand, $\mathrm{Sh}_{\neg\neg}(S)=\mathrm{Sh}(S_0)=\prod_{S_0} \mathrm{Set}$, and if $s$ is a non-principal ultrafilter on $S_0$, then $\varinjlim_{U\ni s} \mathrm{Sh}_{\neg\neg}(U)$ is exactly an ultraproduct of $\mathrm{Set}$ – which may have very similar properties to $\mathrm{Set}$, but is not $\mathrm{Set}$ itself. What is going on?

Answer 1

Yes, this is a model of ETCSR. Unfortunately, I don't know of a proof of this in the literature, which is in general sadly lacking as regards replacement/collection axioms in topos theory. But here's a sketch.

As Zhen says, the filterquotient construction preserves finitary properties such as Booleanness and the axiom of choice. Moreover, a maximal filterquotient will be two-valued. But as you point out, a nondegenerate two-valued topos satisfying the (external) axiom of choice is necessarily well-pointed; I wrote out an abstract proof at https://ncatlab.org/nlab/show/well-pointed+topos#boolean_properties. Thus, $\varinjlim_{U\ni s} \mathrm{Sh}_{\neg\neg}(S)$ is a model of ETCS.

As for replacement, the proof that I know (which is not written out in the literature) goes by way of the notions of "stack semantics" and "autology" in my preprint Stack semantics and the comparison of material and structural set theories (the other half, not the part that became the paper of mine cited in the question).

Briefly, stack semantics is an extension of the internal logic of a topos to a logic containing unbounded quantifiers of the form "for all objects" or "there exists an object". (My current perspective, sketched in these slides, is that this is a fragment of the internal dependent type theory of a 2-topos of stacks -- hence the name!) This language allows us to ask whether a topos is "internally" a model of structural set theories such as ETCS or ETCSR.

It turns out that every topos is "internally (constructively) well-pointed", and moreover satisfies the internal collection axiom schema. But the internal separation axiom schema is a strong condition on the topos, which I called being "autological". If a topos is autological and also Boolean, then the logic of its stack semantics is classical; thus it is internally a model of ETCSR. Since Grothendieck toposes are autological, your $\mathrm{Sh}_{\neg\neg}(S)$ is internally a model of ETCSR.

Now we can also prove that if $\mathcal{E}$ is Boolean and autological, so is any filterquotient of it. The idea is to prove a categorical version of Łoś's theorem for the stack semantics. (I don't know whether this is true without Booleanness, which annoys me to no end, but you probably don't care. (-: ) Therefore, $\varinjlim_{U\ni s} \mathrm{Sh}_{\neg\neg}(S)$ is also autological.

Finally, another fact about autology is that a well-pointed topos is autological if and only if it satisfies the ordinary structural-set-theory axiom schemas of separation and collection. Therefore, $\varinjlim_{U\ni s} \mathrm{Sh}_{\neg\neg}(S)$ satisfies these schemas, hence is a model of ETCSR.

However, I doubt that this particular filterquotient is related to forcing at all. The point is the same one that Jacob made in a comment: when set theorists force over a countable base model to make an "actual" new model, they find an actual generic ultrafilter outside that model. A generic ultrafilter in the base model would be a point of the topos $\mathrm{Sh}_{\neg\neg}(S)$, which as Andreas pointed out in a comment, does not exist. Your "points" $x$ are not points of the topos $\mathrm{Sh}_{\neg\neg}(S)$, so it's unclear to me whether filterquotients at them have anything to do with forcing.

Let me reiterate my argument that the real content of forcing is the internal logic of the topos $\mathrm{Sh}_{\neg\neg}(S)$. In particular, if you build a model of material set theory in this internal logic, what you get is essentially the Boolean-valued model that set theorists talk about. Edit: I think the rest of this answer is off-base; see the discussion in the comments. I'm pretty sure this is the best kind of "model" you can get if you don't want to start talking about countable models of ZFC sitting inside larger ambient models.

At the moment, my best guess for a topos-theoretic gloss on the countable-transitive-model version of forcing is something like the following. Suppose that $E$ is a countable model of ETCSR, containing an internal poset $P$, which we can equip with its double-negation topology. Then treating $E$ as the base topos, we can build $\mathrm{Sh}(P,E)$, a bounded $E$-indexed elementary topos (i.e. "$E$ thinks it is a Grothendieck topos"), which contains the Boolean-valued model associated to $P$ as described above. It is the classifying topos of $P$-generic filters, hence has in general no $E$-points.

But we also have the larger topos $\rm Set$ in which $E$ is countable, and we can consider the externalization $|P|$ which is a poset in $\rm Set$, namely $|P| = E(1,P)$. Then we can build the topos $\mathrm{Sh}(|P|,\rm Set)$ which "really is" a Grothendieck topos and classifies $|P|$-generic filters. The "Rasiowa–Sikorski lemma" implies that, since $E$ is countable, in this case such a filter does actually exist in $\rm Set$, so there is a point $p:\mathrm{Set} \to \mathrm{Sh}(|P|,\rm Set)$.

Now we should also have some kind of "externalization functor" $|-| : \mathrm{Sh}(P,E) \to \mathrm{Sh}(|P|,\rm Set)$. My guess is that the set-theorists' forcing model is the "image" (whatever that means) of the Boolean-valued model in $\mathrm{Sh}(P,E)$ under the composite of this externalization functor with the inverse image functor $p^* : \mathrm{Sh}(|P|,\rm Set) \to Set$. However, I have not managed to make this precise.

Answer 2

I think the language of classifying toposes is helpful in understanding this view of forcing.

Let $P$ be a poset. The set theorists have the intuition that forcing over $P$ adjoins a generic filter of $P$ to the universe, and in a similar way the classifying topos of a theory is what you get by freely adjoining a model of that theory to the base $\textbf{Set}$. Every topos is a classifying topos of some theory, and it turns out that $\textbf{Sh} (P, \lnot \lnot)$ can be regarded as classifying generic filters of $P$ – so, in some sense, a direct translation of the set theorists' intuition!

For convenience – otherwise we will have to use extremely cumbersome circumlocutions – we assume $P$ is a meet semilattice with binary meet $\land$ and top element $\top$. With some work (= mechanical application of Diaconescu's theorem), the topos $\textbf{Psh} (P)$ can be seen to classify models of the following propositional theory:

• We have propositional symbols $\theta_p$ for each $p \in P$.
• We have the axiom $(\theta_{p_1} \land \cdots \land \theta_{p_n}) \implies \theta_q$ whenever $p_1 \land \cdots \land p_n \le q$ in $P$. (The case $n = 0$ means $\theta_\top$ is an axiom.)

A model of this theory consists of subobjects $\Theta_p$ of the terminal object $1$ for each $p \in P$, such that $\Theta_{p_1} \times \cdots \times \Theta_{p_n}$ is a subobject of $\Theta_q$ whenever $p_1 \land \cdots \land p_n \le q$ in $P$. Thus, in $\textbf{Set}$, models are in bijective correspondence with filters of $P$, i.e. subsets of $P$ containing $\top$ and closed under $\land$. We may therefore say that $\textbf{Psh} (P)$ is the classifying topos for filters of $P$.

Subtoposes of a classifying topos correspond to extensions of the theory: the classifying morphism of some model factors through the subtopos if and only if the model satisfies the extended theory. So the topos $\textbf{Sh} (P, \lnot \lnot)$ must classify some special filters of $P$. Say $D \subseteq P$ is dense under $q \in P$ if, for every $p \in D$ we have $p \le q$ and for every $p \le q$ we have $p' \in D$ such that $p' \le p$. With some work (= Diaconescu's theorem again), we see that $\textbf{Sh} (P, \lnot \lnot)$ classifies models satisfying the following extension:

• We have the axiom $\theta_q \implies \bigvee_{p \in D} \theta_p$ whenever $D \subseteq P$ is dense under $q \in P$.

In $\textbf{Set}$, models correspond to generic filters of $P$, i.e. filters $F \subseteq P$ such that if $q \in F$ and $D \subseteq P$ is dense under $q$ then there is $p \in D$ such that $p \in F$. Thus, we may say that $\textbf{Sh} (P, \lnot \lnot)$ classifies generic filters of $P$. (That said, $P$ may not actually have any generic filters in $\textbf{Set}$. This is the whole point of forcing!)

Now onto the filter-quotient stuff. Set theorists actually have a few different ways of thinking about forcing. The one that comes closest to the sheaf topos construction is forcing using boolean-valued models. To extract a $2$-valued model one chooses an ultrafilter $U$ and then reinterprets a proposition as true if its valuation is in $U$ and false otherwise. More generally, if $A$ is the complete boolean algebra of valuations and $U$ is some (not necessarily ultra) filter of $A$, then we have a boolean algebra $A / U$ obtained by quotienting $A$ by the relations $a \le b$ whenever $a \land u \le b$ for some $u \in U$. If $U$ is complete (i.e. closed under infinitary meets) then $A / U$ is furthermore a complete boolean algebra, and given an $A$-valued model $M$ we obtain an $A / U$-valued model $M / U$ by applying the quotient map $A \to A / U$ to the valuations. In the case that $U = \{ a \in A : b \le a \}$ for some $b \in A$, $A / U$ is isomorphic as a poset to $A_b = \{ a \in A : a \le b \}$. For general filters $U$, it is clear that $A / U \cong \varinjlim_{b \in U^\textrm{op}} A_b$. If $U$ is an ultrafilter we also have $M / U \cong \varinjlim_{b \in U^\textrm{op}} M_b$, but here $M_b$ is defined to be the structure obtained by interpreting a proposition to be true if its valuation is $\ge b$ and false otherwise. (Warning: $M_b$ is usually not a model of the theory of interest!) The topos-theoretic filter-quotient construction is the analogue of this construction.

Here, we have some localic boolean topos $\mathcal{E}$ and we take $A$ to be the complete boolean algebra of subobjects of $1$ in $\mathcal{E}$. When $U$ is a filter, the resulting $\mathcal{E} / U$ will inherit finitary structures preserved by the inverse image functor of open embeddings – so $\mathcal{E} / U$ will have finite limits, finite colimits, power objects, exponentials etc. – but I think one has to do some work to verify that properties like, say, the failure of the continuum hypothesis are also inherited. It should go without saying that $\mathcal{E} / U$ will usually fail to be a Grothendieck topos.

Finally, regarding the internal/external distinction. All of the above is from the external perspective – in the sense that $P$ is a poset in the metatheory – and the role of $\textbf{Set}$ is special. But just as the set theorists can apply forcing to the "real" universe of sets, one can construct the topos of $\lnot\lnot$-sheaves on a poset $P$ inside a general boolean elementary topos $\mathcal{S}$. What I do not know is how to (elegantly) internalise the filter-quotient construction in this scenario. One difficulty is that $P$ is a poset internal to $\mathcal{S}$, and if $\mathcal{S}$ is not well pointed then taking the global points of $P$ loses information. It should be doable, though.

Answer 3

Thanks for all the enlightening answers! Let me summarize my understanding now. (Please correct me if I'm saying something stupid!)

First, as explained by Mike Shulman in his answer, the answer to Question 1) is Yes: $\varinjlim_{U\ni s} \mathrm{Sh}_{\neg\neg}(U)$ is a model of ETCSR. So if you, like me, always wanted to have a hands-on understanding of what forcing does, I think you can go with this explicit model (and do away with all meta-mathematical baggage surrounding either boolean models, or countable base models, and generic filters).

It remains to answer Question 2): How is this related to forcing? The answer seems to be that it is a generic extension $\mathrm{Set}_s[G]$ of $\mathrm{Set}_s$ where $\mathrm{Set}_s$ is an elementary extension of $\mathrm{Set}$.

More precisely, recall the concept of "boolean ultrapowers", which is "ultrapowers with Stone-Cech compactifications replaced by a general extremally disconnected profinite set $S$". Namely, given $S\ni s$ as above, and any model $M$ of some first-order theory, we can look at the constant sheaf with value $M$ on $S$ with respect to the double-negation topology, and take its stalk at $s\in S$. (Warning: This is not really a stalk! I.e., $s$ does not define a point of the topos of double-negation sheaves. By "stalk" I just mean the colimit $\varinjlim_{U\ni s}$; equivalently, push forward to usual sheaves on the topological space $S$, and take the stalk there.) This defines a new model $M_s$ of the first-order theory. (If $S$ is the Stone-Cech compactification of $S_0$ and $s\in S$ is an ultrafilter on $S_0$, then the sheafification is taking any open and closed subset $U\subset S$, corresponding to some subset $U_0\subset S_0$, to $\prod_{U_0} M$, and then the stalk is $\varinjlim_{s\in \beta U_0} \prod_{U_0} M$, i.e. an ultraproduct.) This procedure can be applied in particular to a model of ZFC, or a model of ETCSR, with the procedures being equivalent. This construction features prominently in this beautiful article of Hamkins–Seabold.

The Boolean ultrapower $\mathrm{Set}_s$ of $\mathrm{Set}$ (at $s\in S$) is thus given by the stalk at $s\in S$ of the constant sheaf of categories with value $\mathrm{Set}$. The constant sheaf of categories with value $\mathrm{Set}$ is different from set-valued sheaves! However, there is a natural functor, in particular giving a functor $$\mathrm{Set}_s\to \varinjlim_{U\ni s}\mathrm{Sh}_{\neg\neg}(U).$$

As in Zhen Lin's answer, the topos $\mathrm{Sh}_{\neg\neg}(S)$ classifies generic filters $G$. In particular, it contains such a generic filter itself, given by $$ G=\bigsqcup_{U\subset S} U.$$ (Here, $U$ is identified with the sheaf it represents.)

Now I believe that the discussion around Theorem 22 in Hamkins-Seabold should translate into the following statement.

$\mathrm{Set}_s$ is an elementary extension of $\mathrm{Set}$, $G$ is a generic filter over $\mathrm{Set}_s$, and $\varinjlim_{U\ni s} \mathrm{Sh}_{\neg\neg}(U)$ identifies with the generic extension $\mathrm{Set}_s[G]$ of $\mathrm{Set}_s$.

(What is $\mathrm{Set}_s[G]$ here? It corresponds to the (material) forcing extension by $G$ under translating back-and-forth between structural and material set theory.)

Finally, how is all of this related to usual forcing? In usual forcing, one first makes an auxiliary enlargement $V\subset \tilde{V}$ (i.e. $\mathrm{Set}\to \tilde{\mathrm{Set}}$) so that after this enlargement, "there are new elements of $S$" in the sense that the corresponding complete Boolean algebra $B$ admits new homomorphisms $B\to \{0,1\}$. One can then redo the previous construction, but take the stalk at a "new point" $s\in \tilde{S}$ (where $\tilde{S}$ is the spectrum of $B$ in $\tilde{V}$). All of the above should still work in this setting, giving us $\mathrm{Set}\to \mathrm{Set}_s\to \mathrm{Set}_s[G]$. However, if $s$ corresponds to a $V$-generic filter, then it turns out that $\mathrm{Set}_s=\mathrm{Set}$. So in this case the forcing extension is really one of $\mathrm{Set}$ itself, not of an elementary extension.

This also answers my final confusion in the OP: If $S$ is a Stone-Cech compactification, then $\mathrm{Sh}_{\neg\neg}(S)$ is in fact the constant sheaf of categories with value $\mathrm{Set}$, so in particular $G$ already lies in $\mathrm{Set}_s$ for all $s\in S$, and $\mathrm{Set}_s[G]=\mathrm{Set}_s$. Thus, the forcing extension is trivial, but the elementary extension $\mathrm{Set}\to \mathrm{Set}_s$ to the ultrapower remains.

Why does one usually want generic filters? I think the point is that the extension $\mathrm{Set}_s\subset \mathrm{Set}_s[G]$ always preserves ordinals (in its material incarnation). By contrast, $\mathrm{Set}\subset \mathrm{Set}_s$ very much does not, and in fact $\mathrm{Set}_s$ usually has nonstandard integers; in the material incarnation, this leads to non-wellfounded models. So one uses generic filters to make $\mathrm{Set}=\mathrm{Set}_s$.

From the structural point of view, wellfoundedness is not visible, but of course it may still be disconcerting that the extension has nonstandard integers.

Answer 4

I can't really answer your question, since they are outside my field of expertise. But until Mike and others come to answer, let me make a long comment about the following sentence:

Note that in usual presentations of forcing, if one wants to actually build a new model of ZFC, one has to first choose a countable base model $M$.

While true, this is not quite the case in the usual applications of forcing. Indeed, we normally force over the universe. This is really the whole point of forcing: it is internal to the model you're working with, rather than external. The external part is the generic filter (which we can eliminate, if we are willing to forego well-foundedness), but everything else happens inside the model.

The usual presentation of forcing uses models, because the uses of forcing are to prove consistency results. It's easier to apply this to models, than to develop Boolean-valued logic and make arguments about that. The approach via models also clarifies how forcing works, what are the names, and what the forcing relation truly means.

On the other hand, if you're not interested in preserving well-foundedness (and therefore, by extension adding new "ordinals") you can force over the universe with a non-generic filter that meets "enough dense sets", and use it to interpret the names. This will define a class and a binary relation on it, which will interpret correctly "enough of set theory", but will not be well-founded.

This seems odd in the standard context of forcing, since one of the nice properties of forcing is that it doesn't adds ordinals, so it doesn't violate well-foundedness. But if you're looking at sheaves, there's no notion of a well-founded model, so there's no reason to worry about that.