Let me begin by formulating a concrete (if not 100% precise) question, and then I'll explain what my real agenda is.

Two key facts about forcing are (1) the definability of forcing; i.e., the existence of a notion $\Vdash^\star$ (to use Kunen's notation) such that $p\Vdash \phi$ if and only if $(p \Vdash^\star \phi)^M$, and (2) the truth lemma; i.e., anything true in $M[G]$ is forced by some $p\in G$.

I am wondering if there is a way to "axiomatize" these facts by saying what properties forcing must have, without actually introducing a poset or saying that $G$ is a generic filter or that forcing is a statement about all generic filters, etc. And when I say that forcing "must have" these properties, I mean that by using these axioms, we can go ahead and prove that $M[G]$ satisfies ZFC, and only worry later about how to construct something that satisfies the axioms.

Now for my hidden agenda. As some readers know, I have written A beginner's guide to forcing where I try to give a motivated exposition of forcing. But I am not entirely satisfied with it, and I have recently been having some interesting email conversations with Scott Aaronson that have prompted me to revisit this topic.

I am (and I think Scott is) fairly comfortable with the exposition up to the point where one recognizes that it would be nice if one could add some function $F : \aleph_2^M \times \aleph_0 \to \lbrace 0,1\rbrace$ to a countable transitive model $M$ to get a bigger countable transitive model $M[F]$. It's also easy to grasp, by analogy from algebra, that one also needs to add further sets "generated by $F$." And with some more thought, one can see that adding arbitrary sets to $M$ can create contradictions, and that even if you pick an $F$ that is "safe," it's not immediately clear how to add a set that (for example) plays the role of the power set of $F$, since the "true" powerset of $F$ (in $\mathbf{V}$) is clearly the wrong thing to add. It's even vaguely plausible that one might want to introduce "names" of some sort to label the things you want to add, and to keep track of the relations between them, before you commit to saying exactly what these names are names of. But then there seems to be a big conceptual leap to saying, "Okay, so now instead of $F$ itself, let's focus on the poset $P$ of finite partial functions, and a generic filter $G$. And here's a funny recursive definition of $P$-names." Who ordered all that?

In Cohen's own account of the discovery of forcing, he wrote:

There are certainly moments in any mathematical discovery when the resolution of a problem takes place at such a subconscious level that, in retrospect, it seems impossible to dissect it and explain its origin. Rather, the entire idea presents itself at once, often perhaps in a vague form, but gradually becomes more precise.

So a 100% motivated exposition may be a tad ambitious. However, it occurs to me that the following strategy might be fruitful. Take one of the subtler axioms, such as Comprehension or Powerset. We can "cheat" by looking at the textbook proof that $M[G]$ satisfies the axiom. This proof is actually fairly short and intuitive if you are willing to take for granted certain things, such as the meaningfulness of this funny $\Vdash$ symbol and its two key properties (definability and the truth lemma). The question I have is whether we can actually produce a rigorous proof that proceeds "backwards": We don't give the usual definitions of a generic filter or of $\Vdash$ or even of $M[G]$, but just give the bare minimum that is needed to make sense of the proof that $M[G]$ satisfies ZFC. Then we "backsolve" to figure out that we need to introduce a poset and a generic filter in order to construct something that satisfies the axioms.

If this can be made to work, then I think it would greatly help "ordinary mathematicians" grasp the proof. In ordinary mathematics, expanding a structure $M$ to a larger structure $M[G]$ never requires anything as elaborate as the forcing machinery, so it feels like you're getting blindsided by some deus ex machina. Of course the reason is that the axioms of ZFC are so darn complicated. So it would be nice if one could explain what's going on by first looking at what is needed to prove that $M[G]$ satisfies ZFC, and use that to motivate the introduction of a poset, etc.

By the way, I suspect that in practice, many people learn this stuff somewhat "backwards" already. Certainly, on my first pass through Kunen's book, I skipped the ugly technical proof of the definability of forcing and went directly to the proof that $M[G]$ satisfies ZFC. So the question is whether one can push this backwards approach even further, and postpone even the introduction of the poset until after one sees why a poset is needed.

  • 6
    $\begingroup$ Here's a slightly tongue in cheek answer: if the mathematician knows about sheaves, say you are taking some certain sheaves over a site whose objects are the forcing conditions, and then the complicated stuff in forcing comes from a) passing to a two-valued model by a giant quotienting operation and then b) simulating sets as well-founded trees in the result. From the point of view of the forcing relation, you don't do a) and b) but implicitly work with the sheaves, possibly passing to "dense open subsets" in the site (to abuse some language) to show things hold. $\endgroup$
    – David Roberts
    Aug 21, 2020 at 9:45
  • 4
    $\begingroup$ @David: Does that mean that someone can explain sheaves to me in a way that I can understand, just because I understand forcing? :-) $\endgroup$
    – Asaf Karagila
    Aug 21, 2020 at 10:18
  • 1
    $\begingroup$ @DavidRoberts : For such a person, I think the Boolean-valued model approach that I actually took in my paper should be reasonably palatable. Scott Aaronson (among others) found that approach off-putting, so I am trying to find a path that doesn't appeal to multi-valued models. $\endgroup$ Aug 21, 2020 at 14:33
  • 1
    $\begingroup$ I have wondered whether Mac Lane and Moerdijk's book Sheaves in Geometry and Logic has ever helped someone with a background in logic and set theory understand modern geometry. It seemed to be written for people going in the other direction. $\endgroup$ Aug 22, 2020 at 0:27
  • 2
    $\begingroup$ I just wanted to say I already really like the beginners guide you wrote! Please let us know if there will be an improved version $\endgroup$
    – Vincent
    Aug 26, 2020 at 7:45

5 Answers 5


I have proposed such an axiomatization. It is published in Comptes Rendus: Mathématique, which has returned to the Académie des Sciences in 2020 and is now completely open access. Here is a link:


The axiomatization I have proposed is as follows:

Let $(M, \mathbb P, R, \left\{\Vdash\phi : \phi\in L(\in)\right\}, C)$ be a quintuple such that:

  • $M$ is a transitive model of $ZFC$.

  • $\mathbb P$ is a partial ordering with maximum.

  • $R$ is a definable in $M$ and absolute ternary relation (the $\mathbb P$-membership relation, usually denoted by $M\models a\in_p b$).

  • $\Vdash\phi$ is, if $\phi$ is a formula with $n$ free variables, a definable $n+1$-ary predicate in $M$ called the forcing predicate corresponding to $\phi$.

  • $C$ is a predicate (the genericity predicate).

As usual, we use $G$ to denote a filter satisfying the genericity predicate $C$.

Assume that the following axioms hold:

(1) The downward closedness of forcing: Given a formula $\phi$, for all $\overline{a}$, $p$ and $q$, if $M\models (p\Vdash\phi)[\overline{a}]$ and $q\leq p$, then $M\models (q\Vdash\phi)[\overline{a}]$.

(2) The downward closedness of $\mathbb P$-membership: For all $p$, $q$, $a$ and $b$, if $M\models a\in_p b$ and $q\leq p$, then $M\models a\in_q b$.

(3) The well-foundedness axiom: The binary relation $\exists p; M\models a\in_p b$ is well-founded and well-founded in $M$. In particular, it is left-small in $M$, that is, $\left\{a : \exists p; M\models a\in_p b\right\}$ is a set in $M$.

(4) The generic existence axiom: For each $p\in \mathbb P$, there is a generic filter $G$ containing $p$ as an element.

Let $F_G$ denote the transitive collapse of the well-founded relation $\exists p\in G; M\models a\in_p b$.

(5) The canonical naming for individuals axiom: $\forall a\in M;\exists b\in M; \forall G; F_G(b)=a$.

(6) The canonical naming for $G$ axiom: $\exists c\in M;\forall G; F_G(c)= G$.

Let $M[G]$ denote the direct image of $M$ under $F_G$. The next two axioms are the fundamental duality that you have mentioned:

(7) $M[G]\models \phi[F_G(\overline{a})]$ iff $\exists p\in G; M\models (p\Vdash\phi)[\overline{a}]$, for all $\phi$, $\overline{a}$, $G$.

(8) $M\models (p\Vdash\phi)[\overline{a}]$ iff $\forall G\ni p; M[G]\models \phi[F_G(\overline{a})]$, for all $\phi$, $\overline{a}$, $p$.

Finally, the universality of $\mathbb P$-membership axiom.

(9) Given an individual $a$, if $a$ is a downward closed relation between individuals and conditions, then there is a $\mathbb P$-imitation $c$ of $a$, that is, $M\models b\in_p c$ iff $(b,p)\in a$, for all $b$ and $p$.

It follows that $(M, \mathbb P, R, \left\{\Vdash\phi : \phi\in L(\in)\right\}, C, G)$ represent a standard forcing-generic extension: The usual definitions of the forcing predicates can be recovered, the usual definition of genericity can also be recovered ($G$ intersects every dense set in $M$), $M[G]$ is a model of $ZFC$ determined by $M$ and $G$ and it is the least such model. (Axiom $(9)$ is used only in the proof that $M[G]$ is a model).

  • 4
    $\begingroup$ This is excellent! From an expository point of view, I still desire a further "reversal," namely motivating the axioms by the way they are used to prove that $M[G]$ satisfies ZFC, but your work is big step in the direction I was hoping for. $\endgroup$ Aug 20, 2020 at 20:56
  • 2
    $\begingroup$ I have tried to motivated the axioms in terms of control: The standard forcing-generic extension is a uniform adjuction of G, ground controlled by forcing. Axioms (1) to (8) are, I believe, not hard to motivate from this point of view. ( M[G] must be controlled from the ground in order to guarantee that G does not encode special properties one can only see from the outside and which would forbid M[G] to be a model). $\endgroup$ Aug 20, 2020 at 21:11

Great Question! Finally someone asks the simplest questions, which almost invariably are the real critical ones (if I cannot explain a great idea to an intelligent person in minutes, it simply means I do not understand it).

In this case, the idea is one of the greatest in modern history.

Let me start with a historical background: in the 90s I talked with Stan Tennenbaum about Forcing, hoping to (finally!) understand it (did not go too far) . Here is what he told me (not verbatim): during those times,late 50s and very early 60s, several folks were trying their hand to prove independence.

What did they know? They certainly knew that they had to add a set G to the minimal model, and then close up with respect to Godel constructibility operations. So far nothing mysterious: it is a bit like adding a complex number to Q and form an algebraic field.

First blocker: if I add a set G which certainly exists to construct the function you described above, how do I know that M[G] is still a model of ZF?

In algebraic number theory I do not have this issue, I simply take the new number , and throw it into the pot, but here I do. Sets carry along information, and some of this information can be devastating (simple example: suppose that G is gonna tell that the first ordinal outside of M is in fact reachable, that would be very bad news.

All this was known to the smart folks at the time. What they did not know is: very well, I am in a mine field, how then I select my G so it does not create trouble and do what is supposed to do? That is the fundamental question.

They wanted to find G, describe it, and then add it.

Enter Cohen. In a majestic feat of mathematical innovation, Cohen, rather than going into the mine field outside of M searching for the ideal G, enters M. He looks at the world outside, so to speak, from inside (I like to think of him looking at the starry sky, call it V, from his little M).

Rather than finding the mysterious G which floats freely in the hyperspace outside M, he says: ok, suppose I wanted to build G, brick by brick, inside M. After all, I know what is supposed to do for me, right? Problem is, I cannot, because if I could it would be constructible in M, and therefore part of M. Back to square one.

BUT: although G is not constructible in M, all its finite portions are, assuming such a G is available in the outer world. It does not exist in M, but the bricks which make it (in your example all the finite approximation of the function), all of them, are there. Moreover, these finite fragments can be partially ordered, just like little pieces of information: one is sometimes bigger than the other, etc

Of course this order is not total. So, he says, let us describe that partial order, call it P. P is INSIDE M, all of it. Cohen has the bricks, and he knows which brick fit others, to form some pieces of walls here and there, but not the full house, not G. Why? because the glue which attach these pieces all together in a coherent way is not there. M does not know about the glue. Cohen is almost done: he steps out of the model, and bingo! there is plenty of glue.

If I add an ultrafilter, it will assemble consistently all the pieces of information, and I have my model. I do not need to explicitly describe it, it is enough to know that the glue is real (outside). Now we go back to the last insight of Cohen. How does he know that glueing all pieces along the ultrafilter will not "mess things up"? Because, and the funny thing is M knows it, all information coming with G is already reached at some point of the glueing process, so it is available in M.


What I just said about the set of fragments of information, is entirely codable in M. M knows everything, except the glue. It even knows the "forcing relation", in other words it knows that IF M[G] exists, then truth in M[G] corresponds to some piece of information from within forcing it.

LAST NOTE One of my favorite books in Science Fiction was written by the set theorist converted to writer, Dr. Rudy Rucker. The book is called White Light, and is a big celebration of Cantorian Set Theory written by an insider. It just misses one pearl, the most glorious one: Forcing. Who knows, someone here, perhaps you, will write the sequel to White Light and show the splendor of Cohen's idea not only to "ordinary mathematicians" but to everybody...

ADDENDUM: SHELAH's LOGICAL DREAM (see commentary of Tim Chow)

Tim, you have no idea how many thoughts your fantastic post has generated in my mind in the last 20 hours. Shelah's dream can be made reality, but it ain't easy, though now at least I have some clue as to how to begin.

It is the "virus control method": suppose you take M and throw in some G which is living in the truncated V cone where M lives. Add G. The very moment you add it, you are forced to add all sets which are G-constructibles in alpha steps, where alpha is any ordinal in M. Now, let us say that the most lethal viral attack perpetrated by G is that one of these new sets is exactly alpha_0, the first ordinal not in M, in other words G or its definable sets code a well order of type alpha_0.

If one carries out the analysis I have just sketched, the conjecture would be that a G which does not cause any damage is a set which is as close as possible to be definable in M already, in some sense to be made precise,but that goes along Cohen's intuition, namely that although G is not M-constructible, all its fragments are.

If this plan can be implemented, it would show that forcing is indeed unique, unless.... unless some other crazy idea come into play

  • 1
    $\begingroup$ I've found that that model of construction (having little parts, and gluing them together into a whole, according to some instructions) to be a very useful paradigm for solving problems. The additional idea that some infinite processes/concepts keep some of the properties inherent in finite processes/concepts, is also quite useful. (This happens, for instance, in products and coproducts in category theory, all the time. The compactness theorem is another instance of this principle in action.) $\endgroup$ Aug 20, 2020 at 23:04
  • 1
    $\begingroup$ This is a nice account of why forcing works, but I guess I'm trying to ask why something more simple-minded doesn't work. Certainly, pre-Cohen folks can't be faulted for failing to find G, describe it, and add it. That was a hard problem. But Cohen found G and described it. With the benefit of hindsight, why can't we simplify the argument? What is it about the ZFC axioms that seemingly compels us to use such elaborate machinery? $\endgroup$ Aug 21, 2020 at 0:59
  • 2
    $\begingroup$ I am reminded that in Shelah's "Logical Dreams," one of his dreams is to "show that forcing is the unique method in some non-trivial sense." $\endgroup$ Aug 21, 2020 at 12:08
  • 2
    $\begingroup$ Of course I'm still piggy-backing on all the usual machinery to prove that a random function works, but still, it seems suggestive. The mentality has switched from, "We have to be really really careful to avoid a contradiction" to "The burden of proof is on the contradiction to manifest itself." Is this mentality accurate? If so, can it be pushed further? $\endgroup$ Aug 21, 2020 at 12:54
  • 2
    $\begingroup$ @TimothyChow To the point of switching from "generic" to "random", don't they mean essentially the same thing? Cohen started with Cohen forcing over a countable model, where the generic filter corresponds to a real in a particular comeager set. In other words, any real from that comeager set would have worked for his argument, so a "generic" (aka "typical") real works. It was always my impression that this is where the terminology comes from. Random reals work the same way but with measure one sets. $\endgroup$ Aug 21, 2020 at 16:06

This is an expansion of David Roberts's comment. It may not be the sort of answer you thought you were looking for, but I think it is appropriate, among other reasons because it directly addresses your question

if there is a way to "axiomatize" these facts by saying what properties forcing must have.

In fact, modern mathematics has developed a powerful and general language for "axiomatizing properties that objects must have": the use of universal properties in category theory. In particular, universal properties give a precise and flexible way to say what it means to "freely" or "generically" add something to a structure.

For example, suppose we have a ring $R$ and we want to "generically" add a new element. The language of universal properties says that this should be a ring $R[x]$ equipped with a homomorphism $c:R\to R[x]$ and an element $x\in R[x]$ with the following universal property: for any ring $S$ equipped with a homomorphism $f:R\to S$ and an element $s\in S$, there exists a unique homomorphism $h:R[x]\to S$ such that $h\circ c = f$ and $h(x) = s$.

Note that this says nothing about how $R[x]$ might be constructed, or even whether it exists: it's only about how it behaves. But this behavior is sufficient to characterize $R[x]$ up to unique isomorphism, if it exists. And indeed it does exist, but to show this we have to give a construction: in this case we can of course use the ring of formal polynomials $a_n x^n + \cdots + a_1 x + a_0$.

From this perspective, if we want to add a function $F : \aleph_2\times \aleph_0 \to 2$ to a model $M$ of ZFC to obtain a new model $M[F]$, the correct thing to do would be to find a notion of "homomorphism of models" such that $M[F]$ can be characterized by a similar universal property: there would be a homomorphism $c:M\to M[F]$ and an $F : \aleph_2\times \aleph_0 \to 2$ in $M[F]$, such that for any model $N$ equipped with a homomorphism $f:M\to N$ and a $G : \aleph_2\times \aleph_0 \to 2$ in $N$, there is a unique homomorphism $h:M[F]\to N$ such that $h\circ c = f$ and $h(F) = G$.

The problem is that the usual phrasing of ZFC, in terms of a collection of things called "sets" with a membership relation $\in$ satisfying a list of axioms in the language of one-sorted first-order logic, is not conducive to defining such a notion of homomorphism. However, there is an equivalent formulation of ZFC, first given by Lawvere in 1964, that works much better for this purpose. (Amusingly, 1964 is exactly halfway between 1908, when Zermelo first proposed his list of axioms for set theory, and the current year 2020.) In Lawvere's formulation, there is a collection of things called "sets" (although they behave differently than the "sets" in the usual presentation of ZFC) and also a separate collection of things called "functions", which together form a category (i.e. functions have sets as domain and codomain, and can be composed), and satisfy a list of axioms written in the language of category theory. (A recent short introduction to Lawvere's theory is this article by Tom Leinster.)

Lawvere's theory is usually called "ETCS+R" (the "Elementary Theory of the Category of Sets with Replacement"), but I want to emphasize that it is really an entirely equivalent formulation of ZFC. That is, there is a bijection between models of ZFC, up to isomorphism, and models of ETCS+R, up to equivalence of categories. In one direction this is exceedingly simple: given a model of ZFC, the sets and functions therein as usually defined form a model of ETCS+R. Constructing an inverse bijection is more complicated, but the basic idea is the Mostowski collapse lemma: well-founded extensional relations can be defined in ETCS+R, and the relations of this sort in any model of ETCS+R form a model of ZFC.

Since a model of ETCS+R is a structured category, there is a straightforward notion of morphism between models: a functor that preserves all the specified structure. However, this notion of morphism has two defects.

The first is that the resulting category of models of ETCS+R is ill-behaved. In particular, the sort of "free constructions" we are interested in do not exist in it! However, this is a problem of a sort that is familiar in modern structural mathematics: when a category is ill-behaved, often it is because we have imposed too many "niceness" restrictions on its objects, and we can recover a better-behaved category by including more "ill-behaved" objects. For instance, the category of manifolds does not have all limits and colimits, but it sits inside various categories of more general "smooth spaces" that do. The same thing happens here: by dropping two of the axioms of ETCS+R we obtain the notion of an elementary topos, and the category of elementary toposes, with functors that preserve all their structure (called "logical functors"), is much better-behaved. In particular, we can "freely adjoin a new object/morphism" to an elementary topos.

(I am eliding here the issue of the replacement/collection axiom, which is trickier to treat correctly for general elementary toposes. But since my main point is that this direction is a blind alley for the purposes of forcing anyway, it doesn't matter.)

The second problem, however, is that these free constructions of elementary toposes do not have very explicit descriptions. This is important because our goal is not merely to freely adjoin an $F:\aleph_2\times \aleph_0 \to 2$, but to show that the existence of such an $F$ is consistent, and for this purpose we need to know that when we freely adjoin such an $F$ the result is nontrivial. Thus, in addition to characterizing $M[F]$ by a universal property, we need some concrete construction of it that we can inspect to deduce its nontriviality.

This problem is solved by imposing a different niceness condition on the objects of our category and changing the notion of morphism. A Grothendieck topos is an elementary topos that, as a category, is complete and cocomplete and has a small generating set. But, as shown by Giraud's famous theorem, it can equivalently be defined as a cocomplete category with finite limits and a small generating set where the finite limits and small colimits colimits interact nicely. This suggests a different notion of morphism between Grothendieck toposes: a functor preserving finite limits and small colimits. Let's call such a functor a Giraud homomorphism (it's the same as a "geometric morphism", but pointing in the opposite direction).

The category of Grothendieck toposes and Giraud homomorphisms is well-behaved, and in particular we can freely adjoin all sorts of structures to a Grothendieck topos -- specifically, any structure definable in terms of finite limits and arbitrary colimits (called "a model of a geometric theory"). (To be precise, this is a 2-category rather than a category, and the universal properties are up to isomorphism, but this is a detail, and unsurprising given the modern understanding of abstract mathematics.) Moreover, the topos $M[G]$ obtained by freely adjoining a model $G$ of some geometric theory to a Grothendieck topos $M$ -- called the classifying topos of the theory of $G$ -- has an explicit description in terms of $M$-valued "sheaves" on the syntax of the theory of $G$. This description allows us to check, in any particular case, that it is nontrivial. But for other purposes, it suffices to know the universal property of $M[G]$. In this sense, the universal property of a classifying topos is an answer to your question:

when I say that forcing "must have" these properties, I mean that by using these axioms, we can go ahead and prove that $M[G]$ satisfies ZFC, and only worry later about how to construct something that satisfies the axioms.

Only one thing is missing: not every Grothendieck topos is a model of ETCS+R, hence $M[G]$ may not itself directly yield a model of ZFC. We solve this in three steps. First, since ZFC satisfies classical logic rather than intuitionistic logic (the natural logic of categories), we force $M[G]$ to become Boolean. Second, by restricting to "propositional" geometric theories we ensure that the result also satisfies the axiom of choice. Finally, we pass to the "internal logic" of the topos, which is to say that we allow "truth values" lying in its subobject classifier rather than in the global poset of truth values $2$. We thereby get an "internal" model of ETCS+R, and hence also an "internal" model of ZFC.

So where does the complicated machinery in the usual presentation of forcing come from? Mostly, it comes from "beta-reducing" this abstract picture, writing out explicitly the meaning of "well-founded extensional relation internal to Boolean sheaves on the syntax of a propositional geometric theory". The syntax of a propositional geometric theory yields, as its Lindenbaum algebra, a poset. The Boolean sheaves on that poset are, roughly, those that satisfy the usual "denseness" condition in forcing. The "internal logic" valued in the subobject classifier corresponds to the forcing relation over the poset. And the construction of well-founded extensional relations translates to the recursive construction of "names".

(Side note: this yields the "Boolean-valued models" presentation of forcing. The other version, where we take $M$ to be countable inside some larger model of ZFC and $G$ to be an actual generic filter living in that larger model, is, at least to first approximation, an unnecessary complication. By comparison (and in jesting reference to Asaf's answer), if we want to adjoin a new transcendental to the field $\mathbb{Q}$, we can simply construct the field of rational functions $\mathbb{Q}(x)$. From the perspective of modern structural mathematics, all we care about are the intrinsic properties of $\mathbb{Q}(x)$; it's irrelevant whether it happens to be embeddable in some given larger field like $\mathbb{R}$ by setting $x=\pi$.)

The final point is that it's not necessary to do this beta-reduction. As usual in mathematics, we get a clearer conceptual picture, and have less work to do, when working at an appropriate level of abstraction. We prove the equivalence of ZFC and ETCS+R once, abstractly. Similarly, we show that we have an "internal" model of ETCS+R in any Grothendieck topos. These proofs are easier to write and understand in category-theoretic language, using the intrinsic characterization of Grothendieck toposes rather than anything to do with sites or sheaves. With that done, the work of forcing for a specific geometric theory is reduced to understanding the relevant properties of its category of Boolean sheaves, which are simple algebraic structures.

  • 2
    $\begingroup$ This answer gives me a faint, but still better, hope of understanding forcing from a type-theoretic point of view than I've ever had before. Thanks. $\endgroup$ Aug 26, 2020 at 12:25
  • 6
    $\begingroup$ @AsafKaragila The point is that if you instead put in the effort to get over the "universal hump" of learning category theory, you end up at a high enough place that you can see over all other humps without any extra effort. (-:O $\endgroup$ Aug 26, 2020 at 20:04
  • 3
    $\begingroup$ @Asaf Maybe one should view it as the difference between knowing about tensor products, their universal property and multilinear algebra, and knowing about tensors as physicists do, all concrete symbol manipulation and efficient calculation. These two viewpoints are inherently different and achieve different viewpoints. Ideally one learns both! $\endgroup$
    – David Roberts
    Aug 27, 2020 at 1:22
  • 2
    $\begingroup$ @AsafKaragila Sure, any series of requests as to why someone wants something will only go so far, ending perhaps with "I just like it". I'm surprised here it's reached so soon. Even a vague "I have the sense that it may be useful for the next step the field should take" adds something more. And now while writing this I see you are adding such content. $\endgroup$ Aug 27, 2020 at 10:33
  • 3
    $\begingroup$ @AsafKaragila "tell me that forcing should be seen through an algebraic lens" I'm not we are telling you that, the question asked for something that would make sense for people who aren't set theorists. This answer is really not meant for people who understand ZF(C) inside out and force six impossible things before breakfast, but for 'generic mathematicians', in the sense that Kevin Buzzard talks about. At best they know what a category is, and what sets are, but are specialists in neither. $\endgroup$
    – David Roberts
    Aug 27, 2020 at 13:28

I think there are a few things to unpack here.

1. What is the level of commitment from the reader?

Are we talking about a casual reader, say someone in number theory, who is just curious about forcing? Or are we talking about someone who is learning about forcing as a blackbox to use in some other mathematical arguments? Or are we talking about a fledgling set theorist who is learning about forcing so they can use it later?

The level of commitment from the reader dictates the clarity of the analogy, and the complexity of the details.

  • To someone just wanting to learn about forcing, understanding what is "a model of set theory" and what are the basic ideas that genericity represent, along with the fact that the generic extension has some sort of a blueprint internal to ground model, are probably enough.

  • To someone who needs to use forcing as a blackbox, understanding the forcing relation is probably slightly more important, but the specific construction of $\Bbb P$-names is perhaps not as important.

  • Finally, to a set theorist, understanding the ideas behind $\Bbb P$-names is perhaps the biggest step in understanding forcing. From their conception, to their interactions with the ground model, and their interpretation.

These different levels would necessitate different analogies, or perhaps omitting the analogies completely in favour of examples.

2. Some recent personal experience

Just before lockdown hit the UK, I had to give a short talk about my recent work to a general audience of mathematicians, and I had to make the first part accessible to bachelor students. If you're studying some easily accessible problems, that's great. If your recent work was developing iterations of symmetric extensions and using that to obtain global failures of the axiom of choice from known local failures. Not as easy.

I realised when I was preparing for this, that there is an algebraic analogy to forcing. No, not the terrible "$\sqrt2$ is like a generic filter". Instead, if we consider subfields between $\Bbb Q$ and $\Bbb R$, to understand $\Bbb Q(\pi)$ we need to evaluate rational functions in $\Bbb Q(x)$ with $\pi$ in the real numbers.

When developing this analogy I was trying it out on some of the postdocs from representation theory, and two things became apparent:

  1. People in algebra very much resisted the idea that $\Bbb Q(\pi)$ is a subfield of $\Bbb R$. To then it was an abstract field, and it was in fact $\Bbb Q(x)$. It took some tweaking to the exposition to make sure that everyone is on board.

  2. The words "model of set theory" can kill the entire exposition, unless we explain what it is immediately after, or immediately before. Because the biggest problem with explaining forcing to non-experts is that people see set theory as "the mathematical universe", and when you're forcing you suddenly bring in new objects into the universe somehow. And even people who say that they don't think that way, it is sometimes apparent from their questions that they are kind of thinking that way.

There are still problems with the analogy, of course. It is only an analogy after all. For one, the theory of ordered fields is not a particularly strong theory—foundationally speaking—and so it cannot internalise everything (like the polynomials and their fraction field) inside the field itself, this is a sharp contrast to set theory. So what is a model of set theory? It's a set equipped with a binary relation which satisfy some axioms, just like a model of group theory is a set equipped with a binary operator which satisfy some axioms.

But now we can use the idea that every real number in $\Bbb Q(\pi)$ has a "name" of some rational function evaluated with $\pi$. It helps you understand why $\Bbb Q(e)$ and $\Bbb Q(\pi)$ are both possible generic extensions, even though they are very different (one contains $\pi$ and the other does not), and it helps you understand why $\Bbb Q(\pi)$ and $\Bbb Q(\pi+1)$ are both the same field, even though we used a different generic filter, because there is an automorphism moving one generic to the other.

Here is where we can switch to talk about genericity, give example of the binary tree, and what does it mean for a branch to be generic over a model, and how density plays a role.

So in this case, we did not go into the specifics. We only talked about the fact that there is a blueprint of the extension, which behaves a bit like $\Bbb Q(x)$, but because set theory is a more complicated theory, this blueprint is found inside the model rather than a "derivable object from our model".

3. What to do better?

Well, the above analogy was developed over a short period of time, and I will probably continue developing it in the next few years every time I explain someone what is forcing.

Where can we do better? Well, you want to talk about the forcing relation. But that's a tricky bit. My advisor, who is by all accounts a great expositor, had a story about telling some very good mathematician about forcing. Once he uttered "a formula in the language of forcing" the other party seemingly drifted off.

And to be absolutely fair, I too drift off when people talk to me about formulas in the language of forcing. I know the meaning of it, and I understand the importance of it, but just the phrase is as off-putting to the mind as "salted apples cores dinner".

I am certain that for the casual reader, this is unnecessary. We don't need to talk about the language of forcing. We simply need to explain that in a model some things are true and others are false. And the blueprint that we have of the model can determine some of that, but that the elements of the binary tree, or as they are called the conditions of the forcing, can tell us more information. They can give us more information on how the names inside the blueprint behave. Couple this with the opposite direction, that everything that happens in the generic extension, happens for a reason, and you got yourself the fundamental theorem of forcing. Without once mentioning formulas and the language of forcing, or even the forcing relation, in technical terms.

Yes, this is still lacking, and yes this is really just aimed at the casual reader. But it's a first step. It's a way to bring people into the fold, one step at a time. First you have an idea, then you start shaping it, and then you sand off the rough edges, oil, colour, and lacquer, and you've got yourself a cake.

  • 2
    $\begingroup$ These are all very useful ideas and suggestions for explaining forcing, and I will add them to my arsenal of tricks. But as for what audience I have in mind for this specific question, I've had a number of people read my article and "get stuck" at roughly the same point, which to be honest is roughly the same point that I myself get stuck. Namely, why is all this machinery being dragged in? There is of course the a posteriori justification, "because it works." But is there an a priori justification for why it's needed? $\endgroup$ Aug 21, 2020 at 12:24
  • 1
    $\begingroup$ Maybe another way to think about it is that the audience is a theory builder who insists on asking annoyingly basic questions and isn't content with just using forcing as a black box. There may not be too many theory builders out there, but my feeling is that if the theory builder's questions can be answered then it could unlock benefits for other people too. $\endgroup$ Aug 21, 2020 at 12:27
  • 4
    $\begingroup$ If you want to appeal to theory builders you need to engage with other constructions that they might know, where truth is controlled "from below". Things like limits, or anything continuous really. We understand the truth of the limit as a limit of the truth of the sequence/diagram that led to it (in the infinite case, that is). Here it's the same. We want to understand the generic extension, so we need a blueprint, this is where the rational functions help. This motivates the need for names. Why are they complicated? Well, models of ZF are complicated. If you're a theory builder, you'll see. $\endgroup$
    – Asaf Karagila
    Aug 21, 2020 at 12:53
  • 1
    $\begingroup$ I should add that the idea that $\mathbb{Q}(\pi)$ is a subfield of $\mathbb{R}$ seemed very natural to me from the point of view of combinatorial (semi)group theory, where it's often very useful to makes analogous identifications. $\endgroup$ Aug 21, 2020 at 18:53
  • 2
    $\begingroup$ @TimothyChow: Once you replace "field" by "ordered field", the abstract field is now the blueprint, the $\Bbb P$-names, and by choosing which rationals are smaller than $x$ you get a semblance of genericity. (And right here you can see how talking about this analogy made it better.) $\endgroup$
    – Asaf Karagila
    Aug 21, 2020 at 20:22

This answer is quite similar to Rodrigo's but maybe slightly closer to what you want.

Suppose $M$ is a countable transitive model of ZFC and $P\in M$. We want to find a process for adding a subset $G$ of $P$ to $M$, and in the end we want this process to yield a transitive model $M[G]$ with $M\cup \{G\}\subseteq M[G]$ and $\text{Ord}\cap M = \text{Ord}\cap M[G]$.

Obviously not just any set $G$ can be adjoined to $M$ while preserving ZFC, so we our process will only apply to certain "good" sets $G$. We have to figure out what these good sets are.

Let's assume we have a collection $M^P$ of terms for elements of $M[G]$. So for each good $G$, we will have a surjection $i_G : M^P\to M[G]$, interpreting the terms. We will also demand that the definability and truth lemmas hold for the good $G$s. Let's explain our hypotheses on good sets more precisely.

If $\sigma\in M^P$ and $a\in M$, write $p\Vdash \varphi(\sigma,a,\dot G)$ to mean that for all good $G$ with $p\in G$, $M[G]$ satisfies $\varphi(i_G(\sigma),a,G)$.

Definability Hypothesis: for any formula $\varphi$, the class $\{(p,\sigma,a)\in P\times M^P \times M: p\Vdash \varphi(\sigma,a,\dot G)\}$ is definable over $M$.

Truth Hypothesis: for any formula $\varphi$, any good $G$, any $\sigma\in M^P$, and any $a\in M$, if $M[G]\vDash \varphi(i_G(\sigma),a,\dot G)$, then there is some $p\in G$ such that $p\Vdash \varphi(\sigma,a,\dot G)$.

Interpretation Hypothesis: for any set $S\in M$, the set $\{i_G(\sigma) : p\in G\text{ and }(p,\sigma)\in S\}$ belongs to $M[G]$. (This must be true if $M[G]$ is to model ZF assuming $i_G$ is definable over $M[G]$.)

Existence Hypothesis: for any $p\in P$, there is a good $G$ with $p\in G$.

One can use the first three hypotheses to show that $M[G]$ is a model of ZFC.

Now preorder $P$ by setting $p\leq q$ if $p\Vdash q\in \dot G$. Let $\mathbb P = (P,\leq)$. Suppose $D$ is a dense subset of $\mathbb P$. Fix a good $G$. We claim $G$ is an $M$-generic filter on $P$. Let's just check genericity. Let $D$ be a dense subset of $\mathbb P$. Suppose towards a contradiction $D\cap G = \emptyset$. By the truth hypothesis, there is some $p\in G$ such that $p\Vdash D\cap \dot G = \emptyset$. By density, take $q\leq p$ with $q\in D$. By the existence hypothesis, take $H$ with $q\in H$. We have $q\Vdash p\in \dot G$, so $p\in H$. But $p\Vdash D\cap \dot G = \emptyset$, so $D\cap H = \emptyset$. This contradicts that $q\in H$.

  • $\begingroup$ Yes, thank you, this is in the direction I want! $\endgroup$ Aug 21, 2020 at 13:14
  • 1
    $\begingroup$ As someone who has never found forcing intuitive...I lose you at the word “write”. Why do we say “write $p$...” when the definition does not involve $p$? How are we supposed to pronounce this $\dot G$? Why did we switch from figuring out which sets are good to figuring out which $\sigma$ and $a$ satisfy a criterion for all good sets? $\endgroup$
    – Matt F.
    Aug 22, 2020 at 7:56
  • $\begingroup$ @MattF. : I think I can answer the first question, which is that the intent was to say "for all good $G$ containing $p$." $\endgroup$ Aug 22, 2020 at 16:15
  • $\begingroup$ @MattF Thanks for pointing out that typo. The question asks for a way of recovering the forcing machinery from the proof that forcing preserves ZFC. That's all I tried to accomplish in my answer. $\Vdash$ is motivated by a natural question: what can we conclude about a good extension $M[G]$ given that $p\in G$? We allow terms for elements of $M[G]$, elements of $M$, and a constant for $G$. This notation is used to express hypotheses on good $G$. The first three hypotheses are exactly what's required for the short proof that $M[G]$ satisfies ZFC. And $\dot{G}$ is pronounced "gee dot." $\endgroup$ Aug 23, 2020 at 0:28

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.