The exact strength of the class forcing theorem
Gödel–Bernays set theory proves that sufficiently nice (i.e. pretame) class forcings satisfy the forcing theorem—that is, these forcing relations admit forcing relations satisfying the recursive definition of the forcing relation. It follows that statements true in the corresponding forcing extensions are forced and forced statements are true. But there are class forcings for which having their forcing relation exceeds in consistency strength. So does not prove the forcing theorem for all class forcings. This is in contrast to the well-known case of set forcing, where proves the forcing theorem for all set forcings. On the other hand, stronger second-order set theories such as Kelley–Morse set theory prove the forcing theorem for all class forcings, providing an upper bound. What is the exact strength of the class forcing theorem?
I will show that, over , the forcing theorem for all class forcings is equivalent to the principle of elementary transfinite recursion for recursions of height . This is equivalent to the existence of -iterated truth predicates for first-order truth relative to any class parameter; which is in turn equivalent to the existence of truth predicates for the infinitary languages allowing any class parameter . This situates the class forcing theorem precisely in the hierarchy of theories between and .
This is joint work with Victoria Gitman, Joel Hamkins, Peter Holy, and Philipp Schlict from our paper of the same name.