English

The exact strength of the class forcing theorem

Logic 2021-07-01 v2

Abstract

The class forcing theorem, which asserts that every class forcing notion P\mathbb{P} admits a forcing relation P\Vdash_{\mathbb{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\"odel-Bernays set theory GBC to the principle of elementary transfinite recursion ETROrd\text{ETR}_{\text{Ord}} for class recursions of length Ord\text{Ord}. It is also equivalent to the existence of truth predicates for the infinitary languages LOrd,ω(,A)\mathcal{L}_{\text{Ord},\omega}(\in,A), allowing any class parameter AA; to the existence of truth predicates for the language LOrd,Ord(,A)\mathcal{L}_{\text{Ord},\text{Ord}}(\in,A); to the existence of Ord\text{Ord}-iterated truth predicates for first-order set theory Lω,ω(,A)\mathcal{L}_{\omega,\omega}(\in,A); to the assertion that every separative class partial order P\mathbb{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\text{Ord}+1. Unlike set forcing, if every class forcing notion P\mathbb{P} has a forcing relation merely for atomic formulas, then every such P\mathbb{P} 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.

Keywords

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

R2 v1 2026-06-22T20:44:44.702Z