The exact strength of the class forcing theorem
Abstract
The 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\"odel-Bernays set theory GBC 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 GBC and Kelley-Morse set theory KM.
Cite
@article{arxiv.1707.03700,
title = {The exact strength of the class forcing theorem},
author = {Victoria Gitman and Joel David Hamkins and Peter Holy and Philipp Schlicht and Kameryn Williams},
journal= {arXiv preprint arXiv:1707.03700},
year = {2021}
}
Comments
34 pages. Commentary concerning this paper can be made at http://jdh.hamkins.org/class-forcing-theorem