I understand that questions about intuition are usually frowned upon, but I'd really appreciate it if someone could verify (or extend) my intuition about the definition of the forcing relationship.

In particular, the case $p \Vdash x_0 = x_1$ appears tricky to me. The definition states the following (I am assuming that $M$ is a countable transitive model of ZFC); suppose $x$ is a $\mathbb{P}$-name for some forcing notion $\mathbb{P}$ if it comprises ordered pairs where the first cooridnate is another $\mathbb{P}$-name, and the second coordinate is a condition. I follows the standard convention that $p \leq q$ means $p$ is stronger than $q$.

Suppose $\mathbb{P} \in M$ is a forcing notion in some countable transitive model of ZFC. Suppose $p \in \mathbb{P}$ is a condition, and $x_0$ and $x_1$ are $\mathbb{P}$-names. We say $p \Vdash x_0 = x_1$ if the following holds: for any $\langle y,s \rangle \in x_0$ the set $$ \{ q \leq p \mid q \leq s \rightarrow \exists\langle y',s'\rangle \in x_1 (q \leq s' \land q \Vdash y=y') \} $$ is dense below $p$, and vice versa with $x_0$ and $x_1$ swapped symmetrically).

I understand this to mean the following: a condition $p$ forces equality if we can always find an extension $q \leq p$ that, for any element of the first name in question, can find a name in the second name in question, so that $q$ forces equality between those elements. So, effectively, the relation ensures that the interpretations of both names w.r.t. some M-generic filter have the same elements, which would indeed force equality.

Now, this is where my intuition ends. I don't understand what the denseness of sets of conditions has to do with this (although it is clearly crucial). I think understand why this is done recursively (it almost looks like a game where each element of each name checks whether it's realised, and then the respective other name must come up with an element for which conditions force equality; if one name fails to come up with such a name, their interpretations can't be equal).

Apologies if this last paragraph didn't quite make sense, but I am struggling to isoloate what I don't understand. If my comments above are insufficient, please let me know and I'll try and rephrase my lack of understanding.

  • 3
    $\begingroup$ In the last line of your highlighted part, it should say "dense $below$ $p$." $\endgroup$ Mar 3, 2020 at 23:27
  • 1
    $\begingroup$ An equivalent def'n of $p\Vdash x_0=x_1$ is that $(x_0)_G=(x_1)_G$ for $every$ $\Bbb P$-generic filter $G$ over $M$ such that $p\in G$. I recommend Set Theory: An Introduction To Independence Proofs (chapter 7) by Kenneth Kunen. $\endgroup$ Mar 3, 2020 at 23:38
  • 2
    $\begingroup$ Re: Density - the density condition is necessary to make sure that the logic of your forcing model actually comes out classical. If you check out how Boolean-valued models work, and what it means to be a regular open set of the downward order topology on a poset, the density condition falls out immediately. $\endgroup$ Mar 4, 2020 at 0:35
  • 3
    $\begingroup$ You can't have a countable transitive model and PA as a meta-theory. If you're working with ctm's, that means that your meta theory is ZF(C), as your object exists in the set theoretic universe. You might want to talk about the meta-meta-theory being PA, and that's fine, but it's completely irrelevant and unnecessary. $\endgroup$
    – Asaf Karagila
    Mar 4, 2020 at 9:12
  • 3
    $\begingroup$ I have so much to say about this, but so not the time right now. I will try to find an hour or two to write an explanation later. This was a huge difficulty for me as well when I first learned forcing. $\endgroup$
    – Asaf Karagila
    Mar 4, 2020 at 9:13

1 Answer 1


At first pass, it's best to approach the recursive approach to forcing as secondary: namely, it's an alternate (and extremely useful) characterization of the purely semantic definition of forcing.

Suppose $M$ is a c.t.m., $\mathbb{P}\in M$ is a forcing notion, and $G$ is $\mathbb{P}$-generic over $M$. We can as usual define the generic extension $M[G]$ - note that this does not involve any appeal to the forcing notion itself, it's simply a direct recursive construction.

This is actually something we need to amend later on when we talk about forcing over ill-founded models, but ignore that for now.

The forcing notion $\Vdash_\mathbb{P}$ is then defined as follows:

For $p\in\mathbb{P}$ and $\varphi$ a sentence in the forcing language we write $p\Vdash\varphi$ iff for all $G$ which are $\mathbb{P}$-generic over $M$ we have $$p\in G\implies M[G]\models\varphi$$

(or more precisely $M[G]\models\varphi[G]$, where $\varphi[G]$ is the result of replacing each name occurring in $\varphi$ with its evaluation at $G$).

This definition is quite straightforward and well-motivated, and some of its basic properties are easy to check (e.g. $p\Vdash\varphi\vee\psi$ iff for each $q\le p$ there is an $r\le q$ such that either $r\Vdash\varphi$ or $r\Vdash\psi$). However, beyond that it's also horrible to work with, the key issue being that it is not obviously definable within $M$. For forcing to be useful we'll need at a bare minimum that for each sentence $\varphi$ of the forcing language in $M$ the set $\{p\in\mathbb{P}: p\Vdash\varphi\}$ is a set in $M$, and the definition above doesn't suggest that that's the case at all.

This is where the recursive approach to forcing comes in. We're going to sit down and think carefully about the definition of $\Vdash$ with the hope that we can whip up a concrete characterization of it (and indeed we'll be successful). Unsurprisingly there are two fundamental recursions going on here: we have to break high-complexity sentences into lower-complexity sentences, and we have to break high-complexity names into lower-complexity names. The former is much easier, with the somewhat unusual result that pinning down the atomic cases (= equality and elementhood) is much more complicated than going from simple sentences to complicated sentences (= handling Booleans and quantification).

For example, let's look at the case of equality. We have:

  • $p\Vdash\mu=\nu$ iff for all $G\ni p$ generic we have $\mu[G]=\nu[G]$.

  • ... which holds iff for each $G\ni p$ generic and $\langle q,\delta\rangle\in \mu$ there is some $\langle r,\eta\rangle\in \nu$ such that $$q\in G\implies r\in G\wedge \delta[G]=\eta[G],$$ with the "$q\in G\implies$" bit here addressing the fact that if $q\not\in G$ then the pair $\langle q,\delta\rangle$ doesn't get "triggered" and so we don't care what it does (and identically with $\mu$ and $\nu$ flipped).

    • Note the reduction in the complexity of the names involved (from $\mu$ to the $\delta$s and from $\nu$ to the $\eta$s); this is crucial to the definition being recursive as opposed to circular, and is a comforting thing to see.
  • OK, now let's start to peel away the reference to $G$ in the above, shooting instead for a characterization in terms of individual conditions and dense sets. $p\Vdash\mu=\nu$ is just saying that for every $\langle q,\delta\rangle\in \mu$ the situation above is unavoidable by generic filters containing $p$ (and identically with $\mu$ and $\nu$ flipped).

  • Specifically, suppose $r\le p$ and $r\le q$ (so $r$ is something that $p$ so far doesn't rule out and also "triggers $\delta$ in $\mu$"). Then we want there to be some $s\le r$ and some $\langle t,\eta\rangle\in\nu$ such that $s\le t$ (that is, $s$ "triggers $\eta$ in $\nu$") and $s\Vdash\delta=\eta$ (and identically with $\mu$ and $\nu$ flipped).

  • Rephrasing this a bit more snappily, we get the characterization in the OP. This might appear circular at first glance since we've used forcing equality inside the definition of forcing equality, but it's a perfectly valid recursion since we keep going down in rank (the $\delta$s and $\eta$s we look at are coordinates of ordered pairs which are themselves elements of $\mu$ and $\nu$ respectively). The point is that this characterization is obviously expressible in $M$, and it's not hard to prove (externally to $M$) that it in fact coincides with the semantic definition.

Hopefully this indicates how the messy-looking recursive definition of forcing inside $M$ emerges from natural considerations. It's a good idea at this point to similarly whip up a definition of the forcing relation for elementhood; it will go very similarly. (Actually the presentation I learned from treated equality and elementhood by simultaneous recursion; that's also a fine option.)

  • $\begingroup$ Thank you! Most of this makes sense. $\endgroup$
    – MacRance
    Mar 7, 2020 at 1:03
  • $\begingroup$ Just to clarify (and referring back to the definition I posted above), assume $p \Vdash \mu = \nu$. Whenever a name $\delta$ is triggered in $\mu$ by a condition $p$ there is a condition $q \leq p$ that triggers both $\delta$ and another name $\eta$ in $\nu$, and this $q$ forces that $\delta = \eta$. This set of conditions $q$ is dense below $p$, so any generic enough filter will ensure such a $q$ is in $G$, and so we go down the recursion. $\endgroup$
    – MacRance
    Mar 7, 2020 at 1:20

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .