The exact strength of the forcing theorem

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.