### 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”. (under review) arXiv bibTeX

AbstractThe class forcing theorem, which asserts that every class forcing notion admits a forcing relation , 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 to the principle of elementary transfinite recursion for class recursions of length . It is also equivalent to the existence of truth predicates for the infinitary languages , allowing any class parameter ; to the existence of truth predicates for the language ; to the existence of -iterated truth predicates for first-order set theory ; to the assertion that every separative class partial order 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 . Unlike set forcing, if every class forcing notion has a forcing relation merely for atomic formulas, then every such has a uniform forcing relation applicable simultaneously to all formulas. Our results situate the class forcing theorem in the rich hierarchy of theories between and Kelley-Morse set theory .

We shall characterize the exact strength of the class forcing theorem, which asserts that every class forcing notion has a corresponding forcing relation , 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 set forcing, for which one may prove in that every set forcing notion has corresponding forcing relations, with class forcing it is consistent with Gödel-Bernays set theory 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 and much more, and so the consistency strength of the class forcing theorem strictly exceeds , 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 and . It turns out that the class forcing theorem is equivalent over to an attractive collection of several other natural set-theoretic assertions; 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 and and beyond, analyzing the strength of various assertions in second-order set theory, such as the principle of elementary transfinite recursion, the principle of -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 . 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 TheoremThe following are equivalent over Gödel-Bernays set theory.

- The atomic class forcing theorem: every class forcing notion admits forcing relations for atomic formulae and
- The class forcing theorem schema: for each first-order formula in the forcing language, with finitely many class names , there is a forcing relation applicable to this formula and its subformulae
- The uniform first-order class forcing theorem: every class forcing notion admits a uniform forcing relation applicable to all assertions in the first-order forcing language with finitely many class names.
- The uniform infinitary class forcing theorem: every class forcing notion admits a uniform forcing relation applicable to all assertions in the infinitary forcing language with finitely many class names.
- Names for truth predicates: every class forcing notion has a class name and a forcing relation for which is a truth-predicate for the first-order forcing language with finitely many class names .
- Boolean completions: Every class forcing notion , that is, every separative class partial order, admits a Boolean completion , a set-complete class Boolean algebra into which densely embeds.
- The class-join separation principle plus -foundation.
- For every class , there is a truth predicate for .
- For every class , there is a truth predicate for .
- For every class , there is an -iterated truth predicate for .
- The principle of determinacy for clopen class games of rank at most .
- The principle of elementary transfinite recursion for -length recursions of first-order properties, using any class parameter.

`@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},

}