Skip to main content
We’ve updated our Terms of Service. A new AI Addendum clarifies how Stack Overflow utilizes AI interactions.
2 of 2
Added more examples
Joel David Hamkins
  • 246.6k
  • 48
  • 808
  • 1.5k

The situation isn't that any given theorem off the shelf might have a forcing proof, but rather that it is a fascinating situation when one can use forcing to prove a theorem purely about the ground model. For such proofs, one makes a conclusion about the set-theoretic universe $V$ by first going to another universe $V[G]$, and then by analyzing the relationship between $V$ and $V[G]$, making a conclusion purely about $V$.

Let me illustrate with a few concrete examples.

  • There are incomparable Turing degrees. This theorem is usually proved by a combinatorial constructive argument, meeting infinitely many requirements in sequence. However, there is also a soft forcing proof: add two mutually generic Cohen reals $c$ and $d$. By genericity, neither is computable from the other, and so the assertion is true in $V[c][d]$. But the assertion there are incomparable degrees has complexity $\Sigma^1_1$, and hence is absolute to $V$. So the statement is true in $V$, as desired.

  • A similar argument produces an infinite antichain this way, with the further property that any real computable from two of them is outright computable with no oracle. Similarly, one can make conclusions about hyperarithmetic incomparability this way, with a very soft argument essentially without any hyperarithmetic details.

  • Indeed, many constructions in computability theory can be viewed as forcing arguments in this way. Rather than describing a detailed construction meeting certain requirements at certain stages, one shows that the requirements correspond to dense sets in a certain partial order and then appeals to genericity. One could use actual genericity and then absoluteness to claim that the desired objects already exist in the ground model, as I did above, or alternatively just note that there were only countably many dense sets to meet and thus the objects exist by the usual diagonalization.

  • Another example arises in Borel equivalence relation theory, in the result that there is no Borel reduction of $E_0$, the relation of almost-equality on binary sequences, to equality. The classical proof uses ergodic theory, but there is a quick forcing argument. Suppose it did reduce; this fact is absolute to the forcing $V[c]$ adding a Cohen real. Since any finite change in $c$ is still generic, the particular real $w$ that $c$ maps to under the reduction does not depend on $c$, and hence is in the ground model $V$. But the assertion that some real maps to $w$ is absolute, and so $c$ differs finitely from a ground model real, contradiction.

  • Similar forcing arguments yield other non-reductions in Borel equivalence relation theory. For exmple, the relation $E_{set}$ can be treated by the forcing $Coll(\omega,\mathbb{R})$, since any two generic reals for this partial order enumerate the same set, the set of ground model reals.

I think there are numerous examples of ZFC theorems proved via forcing, and I would encourage you to edit your question to explicitly encourage people to post such answers, as I would be very interested to see additional such examples. In this case, the big-list tag might be appropriate.

Joel David Hamkins
  • 246.6k
  • 48
  • 808
  • 1.5k