The exact strength of the class forcing theorem

Abstract

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

34 pages. Commentary concerning this paper can be made at http://jdh.hamkins.org/class-forcing-theorem

Cited by in corpus (4)

• Kelley-Morse set theory does not prove the class Fodor principle
• The Structure of Models of Second-order Set Theories
• Reflection in second-order set theory with abundant urelements bi-interprets a supercompact cardinal
• The set-theoretic universe $V$ is not necessarily a class-forcing extension of HOD