The exact strength of the forcing theorem

Philipp Schlicht , Joel David Hamkins, Peter Holy, Victoria Gitman, Kameryn Williams

Research output: Contribution to journalArticle (Academic Journal)peer-review


The class forcing theorem, which asserts that every class forcing notion P admits a forcing relation forces_P, that is, a relation satisfying the forcing relation recursion—it follows that statements true in the corresponding forc- ing extensions are forced and forced statements are true—is equivalent over Gödel-Bernays set theory GBC to the principle of elementary transfinite recursion ETR_Ord for class recursions of length Ord. It is also equivalent to the existence of truth predicates for the infinitary languages L_Ord,omega(in,A), allowing any class parameter A; to the existence of truth predicates for the language L_Ord,Ord(in, A); to the existence of Ord-iterated truth predicates for first-order set theory L_omega,omega(in,A); to the assertion that every separative class partial order P has a set-complete class Boolean completion; to a class-join sep- aration principle; and to the principle of determinacy for clopen class games of rank at most Ord+1. Unlike set forcing, if every class forcing notion P has a forcing relation merely for atomic formulas, then every such 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.

Original languageEnglish
Pages (from-to)1-37
Number of pages37
JournalJournal of Symbolic Logic
Early online date29 Jul 2020
Publication statusE-pub ahead of print - 29 Jul 2020


Dive into the research topics of 'The exact strength of the forcing theorem'. Together they form a unique fingerprint.

Cite this