The exact strength of the class forcing theorem

PDF   Bibtex   Arχiv

 @ARTICLE{GitmanHamkinsHolySchlichtWilliams:ForcingTheorem, 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}, Note ={Submitted}, EPRINT ={1707.03700}, }

V. Gitman, J. D. Hamkins, P. Holy, P. Schlicht, and K. J. Williams, “The exact strength of the class forcing theorem,” J. Symb. Log., vol. 85, no. 3, pp. 869–905, 2020. Available at: https://doi.org/10.1017/jsl.2019.89

We shall characterize the exact strength of the class forcing theorem, which asserts that every class forcing notion $\mathbb P$ has a corresponding forcing relation $\Vdash_{\mathbb P}$ satisfying the relevant recursive definition. 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-sized forcing, where one may prove in ${\rm ZFC}$ that every set forcing notion $\mathbb P$ has its corresponding forcing relations, in the case of class forcing it is consistent with Gödel-Bernays set theory ${\rm GBC}$ that there is a proper class forcing notion $\mathbb P$ lacking a corresponding forcing relation, even merely for the atomic formulas. For certain forcing notions, the existence of an atomic forcing relation implies ${\rm Con}({\rm ZFC})$ and much more (see [1]), and so the consistency strength of the class forcing theorem goes strictly beyond ${\rm 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 exact strength of the class forcing theorem by situating it in the rich hierarchy of theories between ${\rm GBC}$ and ${\rm KM}$, displayed in part in the above diagram, with the class forcing theorem highlighted in blue. It turns out that the class forcing theorem is equivalent over ${\rm GBC}$ to an attractive collection of several other natural set-theoretic assertions. So it is a robust axiomatic principle.

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 ${\rm GBC}$ and ${\rm KM}$ and beyond, analyzing the strength of various assertions in second-order set theory, such as the principle ${\rm ETR}$ of elementary transfinite recursion, the principle of $\Pi^1_1$-comprehension or the principle of determinacy for clopen class games, and so on. We fit these set-theoretic principles into the hierarchy of theories over the base theory ${\rm GBC}$. The main theorem of this article does exactly this with the class forcing theorem, by finding its exact strength in relation to nearby related theories in this hierarchy.

Specifically, extending the analysis of [1] and (missing reference), we show in our main theorem that the class forcing theorem is equivalent over ${\rm GBC}$ to the principle of elementary transfinite recursion ${\rm ETR}_{\rm Ord}$ for transfinite class recursions of length ${\rm Ord}$; it is equivalent to the existence of a truth predicate for the infinitary language of set theory $\mathcal{L}_{\rm {Ord},\omega}(\in,A)$, with any fixed class parameter $A$; to the existence of a truth predicate in the more generous infinitary language $\mathcal{L}_{\rm {Ord},{\rm Ord}}(\in,A)$; to the existence of ${\rm Ord}$-iterated truth predicates for the first-order language $\mathcal{L}_{\omega,\omega}(\in,A)$; to the existence of set-complete Boolean class completions of any separative class partial order; and to the principle of determinacy for clopen class games of rank at most ${\rm Ord}+1$. We shall prove several of the separations indicated in figure above, such as the fact that the class forcing theorem is strictly stronger in consistency strength than having ${\rm ETR}_\alpha$ simultaneously for all ordinals $\alpha$ and strictly weaker than ${\rm ETR}_{\rm {Ord}\cdot\omega}$. The principle ${\rm ETR}_\omega$ is already sufficient to produce truth predicates for first-order truth, relative to any class parameter. Thus, our results locate the class forcing theorem somewhat finely in the hierarchy of second-order set theories.

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

References

1. P. Holy, R. Krapf, P. Lücke, A. Njegomir, and P. Schlicht, “Class forcing, the forcing theorem and Boolean completions,” J. Symb. Log., vol. 81, no. 4, pp. 1500–1530, 2016.