 V. Gitman, J. D. Hamkins, P. Holy, P. Schichit, and K. Williams, “The exact strength of the class forcing theorem.” (Submitted)
@ARTICLE{GitmanHamkinsHolySchlichtWilliams:ForcingTheorem, AUTHOR= {Victoria Gitman and Joel David Hamkins and Peter Holy and Philipp Schichit and Kameryn Williams}, TITLE= {The exact strength of the class forcing theorem}, PDF={https://boolesrings.org/victoriagitman/files/2017/07/Forcingtheorem.pdf}, Note ={Submitted}, EPRINT ={1707.03700}, }
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 setsized 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ödelBernays 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 KelleyMorse 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 settheoretic assertions. So it is a robust axiomatic principle.
The main theorem is naturally part of the emerging subject we call the reverse mathematics of secondorder set theory, a higher analogue of the perhaps more familiar reverse mathematics of secondorder arithmetic. In this new research area, we are concerned with the hierarchy of secondorder set theories between ${\rm GBC}$ and ${\rm KM}$ and beyond, analyzing the strength of various assertions in secondorder 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 settheoretic 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 [2], 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 firstorder language $\mathcal{L}_{\omega,\omega}(\in,A)$; to the existence of setcomplete 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 firstorder truth, relative to any class parameter. Thus, our results locate the class forcing theorem somewhat finely in the hierarchy of secondorder set theories.
Main Theorem: The following are equivalent over GödelBernays set theory ${\rm GBC}$.
 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.$$

The class forcing theorem scheme: every class forcing notion admits a scheme of forcing relations for firstorder formulas. That is, for any particular firstorder formula in the forcing language (finite in the metatheory), 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.  The uniform firstorder class forcing theorem: every class forcing notion $\mathbb P$ admits a uniform forcing relation $$p\Vdash\varphi(\vec \tau),$$ applicable uniformly with all firstorder 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$.
 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 truthpredicate for the firstorder forcing language with finitely many class name parameters $\mathcal{L}_{\omega,\omega}(\in,V^{\mathbb P},\dot\Gamma_0,\ldots,\dot\Gamma_m)$.
 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$.
 Every class forcing notion $\mathbb P$ admits a Boolean completion $\mathbb B$, a setcomplete class Boolean algebra into which $\mathbb P$ densely embeds.
 The classjoin separation principle plus ${\rm ETR}_{\rm Ord}foundation.
 For every class $A$, there is a truth predicate for $\mathcal{L}_{{\rm Ord},\omega}(\in,A)$.
 For every class $A$, there is a truth predicate for $\mathcal{L}_{{\rm Ord},{\rm Ord}}(\in,A)$.
 For every class $A$, there is an ${\rm Ord}$iterated truth predicate for $\mathcal{L}_{\omega,\omega}(\in,A)$.
 The principle ${\rm ETR}_{\rm Ord}$ of elementary transfinite recursion for ${\rm Ord}$length recursions of firstorder properties, using any class parameter.
 The principle of determinacy for clopen class games of rank at most ${\rm Ord}+1$.
[Bibtex]
@article {PeterHolyRegulaKrapfPhilippLuckeAnaNjegomirPhilippSchlicht:classforcing1,
AUTHOR = {Peter Holy and Regula Krapf and Philipp L\"{u}cke and Ana Njegomir and Philipp Schlicht},
TITLE = {Class Forcing, the Forcing Theorem and Boolean Completions},
NOTE ={To appear in the Journal of Symbolic Logic}
}
[Bibtex]
@article {PeterHolyRegulaKrapfPhilippSchlicht:classforcing2,
AUTHOR = {Peter Holy and Regula Krapf and Philipp Schlicht},
TITLE = {Characterizations of Pretameness and the {O}rdcc},
NOTE ={Preprint}
}
Pingback: The exact strength of the class forcing theorem  Joel David Hamkins