The exact strength of the class forcing theorem

  • V. Gitman, J. D. Hamkins, P. Holy, P. Schlicht, and K. Williams, “The exact strength of the class forcing theorem.” (manuscript under review)  
    @ARTICLE{GitmanHamkinsHolySchlichtWilliams:The-exact-strength-of-the-class-forcing-theorem,
    author = {Victoria Gitman and Joel David Hamkins and Peter Holy and Philipp Schlicht and Kameryn Williams},
    title = {The exact strength of the class forcing theorem},
    journal = {},
    year = {},
    volume = {},
    number = {},
    pages = {},
    month = {},
    note = {manuscript under review},
    abstract = {},
    keywords = {},
    source = {},
    doi = {},
    eprint = {1707.03700},
    archivePrefix = {arXiv},
    primaryClass = {math.LO},
    url = {http://jdh.hamkins.org/class-forcing-theorem},
    }

Abstract. The class forcing theorem, which asserts that every class forcing notion $\newcommand\P{\mathbb{P}}\P$ admits a forcing relation $\newcommand\forces{\Vdash}\forces_\P$, that is, a relation satisfying the forcing relation recursion — it follows that statements true in the corresponding forcing extensions are forced and forced statements are true — is equivalent over Gödel-Bernays set theory GBC to the principle of elementary transfinite recursion $\newcommand\Ord{\text{Ord}}\newcommand\ETR{\text{ETR}}\ETR_{\Ord}$ for class recursions of length $\Ord$. It is also equivalent to the existence of truth predicates for the infinitary languages $\mathcal{L}_{\Ord,\omega}(\in,A)$, allowing any class parameter $A$; to the existence of truth predicates for the language $\mathcal{L}_{\Ord,\Ord}(\in,A)$; to the existence of $\Ord$-iterated truth predicates for first-order set theory $\mathcal{L}_{\omega,\omega}(\in,A)$; to the assertion that every separative class partial order $\P$ has a set-complete class Boolean completion; to a class-join separation principle; and to the principle of determinacy for clopen class games of rank at most $\Ord+1$. Unlike set forcing, if every class forcing relation $\P$ has a forcing relation merely for atomic formulas, then every such $\P$ has a uniform forcing relation that applies uniformly to all formulas. Our results situate the class forcing theorem in the rich hierarchy of theories between GBC and Kelley-Morse set theory KM.

We shall characterize the exact strength of the class forcing theorem, which asserts that every class forcing notion $\P$ has a corresponding forcing relation $\forces_\P$, a relation satisfying the forcing relation recursion. When there is such a forcing relation, then statements true in any corresponding forcing extension are forced and forced statements are true in those extensions.

Unlike the case of set forcing, where one may prove in ZFC that every set forcing notion has corresponding forcing relations, for class forcing it is consistent with Gödel-Bernays set theory GBC that there is a proper class forcing notion lacking a corresponding forcing relation, even merely for the atomic formulas. For certain forcing notions, the existence of an atomic forcing relation implies Con(ZFC) and much more, and so the consistency strength of the class forcing theorem strictly exceeds GBC, if this theory is consistent. Nevertheless, the class forcing theorem is provable in stronger theories, such as Kelley-Morse set theory. What is the exact strength of the class forcing theorem?

Our project here is to identify the strength of the class forcing theorem by situating it in the rich hierarchy of theories between GBC and KM, displayed in part in the figure above, with the class forcing theorem highlighted in blue. It turns out that the class forcing theorem is equivalent over GBC to an attractive collection of several other natural set-theoretic assertions; it is a robust axiomatic principle.

Hierarchy between GBC and KM

The main theorem is naturally part of the emerging subject we call the reverse mathematics of second-order set theory, a higher analogue of the perhaps more familiar reverse mathematics of second-order arithmetic. In this new research area, we are concerned with the hierarchy of second-order set theories between GBC and KM and beyond, analyzing the strength of various assertions in second-order set theory, such as the principle ETR of elementary transfinite recursion, the principle of $\Pi^1_1$-comprehension or the principle of determinacy for clopen class games. We fit these set-theoretic principles into the hierarchy of theories over the base theory GBC. The main theorem of this article does exactly this with the class forcing theorem by finding its exact strength in relation to nearby theories in this hierarchy.

Main Theorem. The following are equivalent over Gödel-Bernays set theory.

  1. The atomic class forcing theorem: every class forcing notion admits forcing relations for atomic formulas $$p\forces\sigma=\tau\qquad\qquad p\forces\sigma\in\tau.$$
  2. The class forcing theorem scheme: for each first-order formula $\varphi$ in the forcing language, with finitely many class names $\dot \Gamma_i$, there is a forcing relation applicable to this formula and its subformulas
    $$p\forces\varphi(\vec \tau,\dot\Gamma_0,\ldots,\dot\Gamma_m).$$
  3. The uniform first-order class forcing theorem: every class forcing notion $\P$ admits a uniform forcing relation $$p\forces\varphi(\vec \tau),$$ applicable to all assertions $\varphi$ in the first-order forcing language with finitely many class names $\mathcal{L}_{\omega,\omega}(\in,V^\P,\dot\Gamma_0,\ldots,\dot\Gamma_m)$.
  4. The uniform infinitary class forcing theorem: every class forcing notion $\P$ admits a uniform forcing relation $$p\forces\varphi(\vec \tau),$$ applicable to all assertions $\varphi$ in the infinitary forcing language with finitely many class names $\mathcal{L}_{\Ord,\Ord}(\in,V^\P,\dot\Gamma_0,\ldots,\dot\Gamma_m)$.
  5. Names for truth predicates: every class forcing notion $\P$ has a class name $\newcommand\T{{\rm T}}\dot\T$ and a forcing relation for which $1\forces\dot\T$ is a truth-predicate for the first-order forcing language with finitely many class names $\mathcal{L}_{\omega,\omega}(\in,V^\P,\dot\Gamma_0,\ldots,\dot\Gamma_m)$.
  6. Every class forcing notion $\P$, that is, every separative class partial order, admits a Boolean completion $\mathbb{B}$, a set-complete class Boolean algebra into which $\P$ densely embeds.
  7. The class-join separation principle plus $\ETR_{\Ord}$-foundation.
  8. For every class $A$, there is a truth predicate for $\mathcal{L}_{\Ord,\omega}(\in,A)$.
  9. For every class $A$, there is a truth predicate for $\mathcal{L}_{\Ord,\Ord}(\in,A)$.
  10. For every class $A$, there is an $\Ord$-iterated truth predicate for $\mathcal{L}_{\omega,\omega}(\in,A)$.
  11. The principle of determinacy for clopen class games of rank at most $\Ord+1$.
  12. The principle $\ETR_{\Ord}$ of elementary transfinite recursion for $\Ord$-length recursions of first-order properties, using any class parameter.

Implication cycle 12

We prove the theorem by establishing the complete cycle of indicated implications. The red arrows indicate more difficult or substantive implications, while the blue arrows indicate easier or nearly immediate implications. The green dashed implication from statement (12) to statement (1), while not needed for the completeness of the implication cycle, is nevertheless used in the proof that (12) implies (4). The proof of (12) implies (7) also uses (8), which follows from the fact that (12) implies (9) implies (8).

For more, download the paper from the arxiv:

  • V. Gitman, J. D. Hamkins, P. Holy, P. Schlicht, and K. Williams, “The exact strength of the class forcing theorem.” (manuscript under review)  
    @ARTICLE{GitmanHamkinsHolySchlichtWilliams:The-exact-strength-of-the-class-forcing-theorem,
    author = {Victoria Gitman and Joel David Hamkins and Peter Holy and Philipp Schlicht and Kameryn Williams},
    title = {The exact strength of the class forcing theorem},
    journal = {},
    year = {},
    volume = {},
    number = {},
    pages = {},
    month = {},
    note = {manuscript under review},
    abstract = {},
    keywords = {},
    source = {},
    doi = {},
    eprint = {1707.03700},
    archivePrefix = {arXiv},
    primaryClass = {math.LO},
    url = {http://jdh.hamkins.org/class-forcing-theorem},
    }

See also Victoria’s post, Kameryn’s post.

The definable cut of a model of set theory can be changed by small forcing

Cupid carving his bow -- ParmigianinoIf $M$ is a model of ZFC set theory, let $I$ be the definable cut of its ordinals, the collection of ordinals that are below an ordinal $\delta$ of $M$ that is definable in $M$ without parameters. This would include all the ordinals of $M$, if the definable ordinals happen to be unbounded in $M$, but one can also construct examples where the definable cut is bounded in $M$.  Let $M_I$ be the corresponding definable cut of $M$ itself, the rank-initial segment of $M$ determined by $I$, or in other words, the collection of all sets $x$ in $M$ of rank below a definable ordinal of $M$. Equivalently, $$M_I=\bigcup_{\delta\in I} V_\delta^M.$$ It is not difficult to see that this is an elementary substructure $M_I\prec M$, because we can verify the Tarski-Vaught criterion as follows. If $M\models\exists y\ \varphi(x,y)$, where $x\in M_I$, then let $\delta$ be a definable ordinal above the rank of $x$. In this case, the ordinal $\theta$, which is the supremum over all $a\in V_\delta$ of the minimal rank of a set $y$ for which $\varphi(a,y)$, if there is such a $y$. This supremum $\theta$ is definable, and so since $x\in V_\delta$, the minimal rank of a $y$ such that $\varphi(x,y)$ is at most $\theta$. Consequently, since $\theta\in I$, such a $y$ can be found in $M_I$. So we have found the desired witness inside the substructure, and so it is elementary $M_I\prec M$. Note that in the general case, one does not necessarily know that $I$ has a least upper bound in $M$. Under suitable assumptions, it can happen that $I$ is unbounded in $M$, that $I$ is an ordinal of $M$, or that $I$ is bounded in $M$, but has no least upper bound.

What I am interested in for this post is how the definable cut might be affected by forcing. Of course, it is easy to see that if $M$ is definable in $M[G]$, then the definable cut of $M[G]$ is at least as high as the definable cut of $M$, simply because the definable ordinals of $M$ remain definable in $M[G]$.

A second easy observation is that if the definable cut of $M$ is bounded in $M$, then we could perform large collapse forcing, collapsing a cardinal above $I$ to $\omega$, which would of course make every cardinal of $I$ countable in the extension $M[G]$. In this case, since $\omega_1^{M[G]}$ is definable, it would change the definable cut. So this kind of very large forcing can change the definable cut, making it larger.

But what about small forcing? Suppose that the forcing notion $\newcommand\P{\mathbb{P}}\P$ we intend to forcing with is small in the sense that it is in the definable cut $M_I$. This would be true if $\P$ itself were definable, for example, but really we only require that $\P$ has rank less than some definable ordinal of $M$. Can this forcing change the definable cut?

Let me show at least that the definable cut can never go up after small forcing.

Theorem. If $G\subset\P$ is $M$-generic for forcing $\P$ in the definable cut of $M$, then the definable cut of $M[G]$ is below or the same in the ordinals as it was in $M$.

Proof. Suppose that $G\subset\P$ is $M$-generic, and we consider the forcing extension $M[G]$. We have already proved that $M_I\prec M$ is an elementary submodel. I claim that this relation lifts to the forcing extension $M_I[G]\prec M[G]$. Note first that since $\P\in M_I$ and $M_I$ is a rank initial segment of $M$, it follows that $M_I$ has all the subsets of $\P$ in $M$, and so $G$ is $M_I$-generic. So the extension $M_I[G]$ makes sense. Next, suppose that $M[G]\models\varphi(a)$ for some $a\in M_I[G]$. If $\dot a$ is a name for $a$ in $M_I$, then there is some condition $p\in G$ forcing $\varphi(\dot a)$ over $M$. Since $M_I\prec M$, this is also forced by $p$ over $M_I$, and thus $M_I[G]\models\varphi(a)$ as well, as desired. So $M_I[G]\prec M[G]$, and from this it follows that every definable ordinal of $M[G]$ is in the cut $I$. So the definable cut did not get higher. QED

But can it go down? Not if the model $M$ is definable in $M[G]$, by our earlier easy observation. Consequently,

Theorem. If $M$ is definable in $M[G]$, where $G\subset\P$ is $M$-generic for forcing $\P$ below the definable cut of $M$, then the definable cut of $M[G]$ is the same as the definable cut of $M$.

Proof. It didn’t go down, since $M$ is definable in $M[G]$; and it didn’t go up, since $\P$ was small. QED

What if $M$ is not definable in $M[G]$? Can we make the definable cut go down after small forcing? The answer is yes.

Theorem. If ZFC is consistent, then there is a model $M\models\text{ZFC}$ with a definable notion of forcing $\P$ (hence in the definable cut of $M$), such that if $G\subset\P$ is $M$-generic, then the definable cut of the forcing extension $M[G]$ is strictly shorter than the definable cut of $M[G]$.

Proof. Start with a model of $\text{ZFC}+V=L$, whose definable ordinals are bounded by a cardinal $\delta$. Let’s call it $L$, and let $I$ be the definable cut of $L$, which we assume is bounded by $\delta$. Let $M=L[G]$ be the forcing extension of $L$ obtained by performing an Easton product, adding a Cohen subset to every regular cardinal above $\delta$ in $L$. Since this forcing adds no sets below $\delta$, but adds a Cohen set at $\delta^+$, it follows that $\delta$ becomes definable in $L[G]$. In fact, since the forcing is homogeneous and definable from $\delta$, it follows that the definable ordinals of $L[G]$ are precisely the ordinals that are definable in $L$ with parameter $\delta$. These may be bounded or unbounded in $L[G]$. Now, let $\newcommand\Q{\mathbb{Q}}\Q$ be the Easton product forcing at the stages below $\delta$, and suppose that $G\subset\Q$ is $L[G]$-generic. Consider the model $L[G][H]$. Note that the forcing $\Q$ is definable in $L[G]$, since $\delta$ is definable there. This two-step forcing can be combined into one giant Easton product in $L$, the product that simply forces to add a Cohen subset to every regular cardinal. Since this version of the forcing is homogeneous and definable in $L$, it follows that the definable ordinals of $L[G][H]$ are precisely the definable ordinals of $L$, which are bounded by $I$. In summary, the definable cut of $L[G]$ is strictly above $\delta$, since $\delta$ is definable in $L[G]$, and the forcing $\Q$ has size and rank $\delta$; but the forcing extension $L[G][H]$ has definable cut $I$, which is strictly bounded by $\delta$. So the definable cut was made smaller by small forcing, as claimed. QED

This post is an account of some ideas that Alexander Block and I had noted today during the course of our mathematical investigation of another matter.

Regula Krapf, Ph.D. 2017, University of Bonn

Regula Krapf successfully defended her PhD dissertation January 12, 2017 at the University of Bonn, with a dissertation entitled, “Class forcing and second-order arithmetic.”  I was a member of the dissertation examining committee. Peter Koepke was the dissertation supervisor.

Regula Krapf

Regula Krapf, Class forcing and second-order arithmetic, dissertation 2017, University of Bonn. (Slides)

Abstract. We provide a framework in a generalization of Gödel-Bernays set theory for performing class forcing. The forcing theorem states that the forcing relation is a (definable) class in the ground model (definability lemma) and that every statement that holds in a class-generic extension is forced by a condition in the generic filter (truth lemma). We prove both positive and negative results concerning the forcing theorem. On the one hand, we show that the definability lemma for one atomic formula implies the forcing theorem for all formulae in the language of set theory to hold. Furthermore, we introduce several properties which entail the forcing theorem. On the other hand, we give both counterexamples to the definability lemma and the truth lemma. In set forcing, the forcing theorem can be proved for all forcing notions by constructing a unique Boolean completion. We show that in class forcing the existence of a Boolean completion is essentially equivalent to the forcing theorem and, moreover, Boolean completions need not be unique.

The notion of pretameness was introduced to characterize those forcing notions which preserve the axiom scheme of replacement. We present several new characterizations of pretameness in terms of the forcing theorem, the preservation of separation, the existence of nice names for sets of ordinals and several other properties. Moreover, for each of the aforementioned properties we provide a corresponding characterization of the Ord-chain condition.

Finally, we prove two equiconsistency results which compare models of ZFC (with large cardinal properties) and models of second-order arithmetic with topological regularity properties (and determinacy hypotheses). We apply our previous results on class forcing to show that many important arboreal forcing notions preserve the $\Pi^1_1$-perfect set property over models of second-order arithmetic and also give an example of a forcing notion which implies the $\Pi^1_1$-perfect set property to fail in the generic extension.

Regula has now taken up a faculty position at the University of Koblenz.