# The exact strength of the class forcing theorem


We shall characterize the exact strength of the class forcing theorem, which asserts that every class forcing notion $\P$ has a corresponding forcing relation $\forces_\P$, a relation satisfying the forcing relation recursion. When there is such a forcing relation, then statements true in any corresponding forcing extension are forced and forced statements are true in those extensions.

Unlike the case of set forcing, where one may prove in ZFC that every set forcing notion has corresponding forcing relations, for class forcing it is consistent with Gödel-Bernays set theory GBC that there is a proper class forcing notion lacking a corresponding forcing relation, even merely for the atomic formulas. For certain forcing notions, the existence of an atomic forcing relation implies Con(ZFC) and much more, and so the consistency strength of the class forcing theorem strictly exceeds GBC, if this theory is consistent. Nevertheless, the class forcing theorem is provable in stronger theories, such as Kelley-Morse set theory. What is the exact strength of the class forcing theorem?

Our project here is to identify the strength of the class forcing theorem by situating it in the rich hierarchy of theories between GBC and KM, displayed in part in the figure above, with the class forcing theorem highlighted in blue. It turns out that the class forcing theorem is equivalent over GBC to an attractive collection of several other natural set-theoretic assertions; it is a robust axiomatic principle.

The main theorem is naturally part of the emerging subject we call the reverse mathematics of second-order set theory, a higher analogue of the perhaps more familiar reverse mathematics of second-order arithmetic. In this new research area, we are concerned with the hierarchy of second-order set theories between GBC and KM and beyond, analyzing the strength of various assertions in second-order set theory, such as the principle ETR of elementary transfinite recursion, the principle of $\Pi^1_1$-comprehension or the principle of determinacy for clopen class games. We fit these set-theoretic principles into the hierarchy of theories over the base theory GBC. The main theorem of this article does exactly this with the class forcing theorem by finding its exact strength in relation to nearby theories in this hierarchy.

Main Theorem. The following are equivalent over Gödel-Bernays set theory.

1. The atomic class forcing theorem: every class forcing notion admits forcing relations for atomic formulas $$p\forces\sigma=\tau\qquad\qquad p\forces\sigma\in\tau.$$
2. The class forcing theorem scheme: for each first-order formula $\varphi$ in the forcing language, with finitely many class names $\dot \Gamma_i$, there is a forcing relation applicable to this formula and its subformulas
$$p\forces\varphi(\vec \tau,\dot\Gamma_0,\ldots,\dot\Gamma_m).$$
3. The uniform first-order class forcing theorem: every class forcing notion $\P$ admits a uniform forcing relation $$p\forces\varphi(\vec \tau),$$ applicable to all assertions $\varphi$ in the first-order forcing language with finitely many class names $\mathcal{L}_{\omega,\omega}(\in,V^\P,\dot\Gamma_0,\ldots,\dot\Gamma_m)$.
4. The uniform infinitary class forcing theorem: every class forcing notion $\P$ admits a uniform forcing relation $$p\forces\varphi(\vec \tau),$$ applicable to all assertions $\varphi$ in the infinitary forcing language with finitely many class names $\mathcal{L}_{\Ord,\Ord}(\in,V^\P,\dot\Gamma_0,\ldots,\dot\Gamma_m)$.
5. Names for truth predicates: every class forcing notion $\P$ has a class name $\newcommand\T{{\rm T}}\dot\T$ and a forcing relation for which $1\forces\dot\T$ is a truth-predicate for the first-order forcing language with finitely many class names $\mathcal{L}_{\omega,\omega}(\in,V^\P,\dot\Gamma_0,\ldots,\dot\Gamma_m)$.
6. Every class forcing notion $\P$, that is, every separative class partial order, admits a Boolean completion $\mathbb{B}$, a set-complete class Boolean algebra into which $\P$ densely embeds.
7. The class-join separation principle plus $\ETR_{\Ord}$-foundation.
8. For every class $A$, there is a truth predicate for $\mathcal{L}_{\Ord,\omega}(\in,A)$.
9. For every class $A$, there is a truth predicate for $\mathcal{L}_{\Ord,\Ord}(\in,A)$.
10. For every class $A$, there is an $\Ord$-iterated truth predicate for $\mathcal{L}_{\omega,\omega}(\in,A)$.
11. The principle of determinacy for clopen class games of rank at most $\Ord+1$.
12. The principle $\ETR_{\Ord}$ of elementary transfinite recursion for $\Ord$-length recursions of first-order properties, using any class parameter.

We prove the theorem by establishing the complete cycle of indicated implications. The red arrows indicate more difficult or substantive implications, while the blue arrows indicate easier or nearly immediate implications. The green dashed implication from statement (12) to statement (1), while not needed for the completeness of the implication cycle, is nevertheless used in the proof that (12) implies (4). The proof of (12) implies (7) also uses (8), which follows from the fact that (12) implies (9) implies (8).

# The mate-in-n problem of infinite chess is decidable

• D. Brumleve, J. D. Hamkins, and P. Schlicht, “The Mate-in-$n$ Problem of Infinite Chess Is Decidable,” in How the World Computes, S. Cooper, A. Dawar, and B. Löwe, Eds., Springer, 2012, vol. 7318, pp. 78-88.
[Bibtex]
@incollection{BrumleveHamkinsSchlicht2012:TheMateInNProblemOfInfiniteChessIsDecidable,
year= {2012},
isbn= {978-3-642-30869-7},
booktitle= {{How the World Computes}},
volume= {7318},
series= {Lecture Notes in Computer Science},
editor= {Cooper, S.~Barry and Dawar, Anuj and Löwe, Benedikt},
doi= {10.1007/978-3-642-30870-3_9},
title= {The Mate-in-$n$ Problem of Infinite Chess Is Decidable},
url= {http://wp.me/p5M0LV-f8},
publisher= {Springer},
author= {Brumleve, Dan and Hamkins, Joel David and Schlicht, Philipp},
pages= {78-88},
eprint = {1201.5597},
archivePrefix = {arXiv},
primaryClass = {math.LO},
}

Infinite chess is chess played on an infinite edgeless chessboard. The familiar chess pieces move about according to their usual chess rules, and each player strives to place the opposing king into checkmate. The mate-in-$n$ problem of infinite chess is the problem of determining whether a designated player can force a win from a given finite position in at most $n$ moves. A naive formulation of this problem leads to assertions of high arithmetic complexity with $2n$ alternating quantifiers—*there is a move for white, such that for every black reply, there is a countermove for white*, and so on. In such a formulation, the problem does not appear to be decidable; and one cannot expect to search an infinitely branching game tree even to finite depth.

Nevertheless, the main theorem of this article, confirming a conjecture of the first author and C. D. A. Evans, establishes that the mate-in-$n$ problem of infinite chess is computably decidable, uniformly in the position and in $n$. Furthermore, there is a computable strategy for optimal play from such mate-in-$n$ positions. The proof proceeds by showing that the mate-in-$n$ problem is expressible in what we call the first-order structure of chess, which we prove (in the relevant fragment) is an automatic structure, whose theory is therefore decidable. Unfortunately, this resolution of the mate-in-$n$ problem does not appear to settle the decidability of the more general winning-position problem, the problem of determining whether a designated player has a winning strategy from a given position, since a position may admit a winning strategy without any bound on the number of moves required. This issue is connected with transfinite game values in infinite chess, and the exact value of the omega one of chess $\omega_1^{\frak{Ch}}$ is not known.

Richard Stanley’s question on mathoverflow: Decidability of chess on infinite board?