The hierarchy of second-order set theories between GBC and KM and beyond

This will be a talk at the upcoming International Workshop in Set Theory at the Centre International de Rencontres Mathématiques at the Luminy campus in Marseille, France, October 9-13, 2017.

Abstract. Recent work has clarified how various natural second-order set-theoretic principles, such as those concerned with class forcing or with proper class games, fit into a new robust hierarchy of second-order set theories between Gödel-Bernays GBC set theory and Kelley-Morse KM set theory and beyond. For example, the principle of clopen determinacy for proper class games is exactly equivalent to the principle of elementary transfinite recursion ETR, strictly between GBC and GBC+$\Pi^1_1$-comprehension; open determinacy for class games, in contrast, is strictly stronger; meanwhile, the class forcing theorem, asserting that every class forcing notion admits corresponding forcing relations, is strictly weaker, and is exactly equivalent to the fragment $\text{ETR}_{\text{Ord}}$ and to numerous other natural principles. What is emerging is a higher set-theoretic analogue of the familiar reverse mathematics of second-order number theory.

Second-order transfinite recursion is equivalent to Kelley-Morse set theory over GBC

A few years ago, I had observed after hearing a talk by Benjamin Rin that the principle of first-order transfinite recursion for set well-orders is equivalent to the replacement axiom over Zermelo set theory, and thus we may take transfinite recursion as a fundamental set-theoretic principle, one which yields full ZFC when added to Zermelo’s weaker theory (plus foundation).

In later work, Victoria Gitman and I happened to prove that the principle of elementary transfinite recursion ETR, which allows for first-order class recursions along proper class well-orders (not necessarily set-like) is equivalent to the principle of determinacy for clopen class games [1]. Thus, once again, a strong recursion principle exhibited robustness as a fundamental set-theoretic principle.

The theme continued in recent joint work on the class forcing theorem, in which Victoria Gitman, myself, Peter Holy, Philipp Schlicht and Kameryn Williams [2] proved that the principle $\text{ETR}_{\text{Ord}}$, which allows for first-order class recursions of length $\text{Ord}$, is equivalent to twelve natural set-theoretic principles, including the existence of forcing relations for class forcing notions, the existence of Boolean completions for class partial orders, the existence of various kinds of truth predicates for infinitary logics, the existence of $\text{Ord}$-iterated truth predicates, and to the principle of determinacy for clopen class games of rank at most $\text{Ord}+1$.

A few days ago, a MathOverflow question of Alec Rhea’s — Is there a stronger form of recursion? — led me to notice that one naturally gains additional strength by pushing the recursion principles further into second-order set theory.

So let me introduce the second-order recursion principle STR and make the comparatively simple observation that over Gödel-Bernays GBC set theory this is equivalent to Kelley-Morse set theory KM. Thus, we may take this kind of recursion as a fundamental set-theoretic principle.

Definition. In the context of second-order set theory, the principle of second-order transfinite recursion, denoted STR, asserts of any formula $\varphi$ in the second-order language of set theory, that if $\Gamma=\langle I,\leq_\Gamma\rangle$ is any class well-order and $Z$ is any class parameter, then there is a class $S\subset I\times V$ that is a solution of the recursion, in the sense that
$$S_i=\{\ x\ \mid\ \varphi(x,S\upharpoonright i,Z)\ \}$$
for every $i\in I$, where where $S_i=\{\ x\ \mid\ (i,x)\in S\ \}$ is the section on coordinate $i$ and where $S\upharpoonright i=\{\ (j,x)\in S\ \mid\ j<_\Gamma i\ \}$ is the part of the solution at stages below $i$ with respect to $\Gamma$.

Theorem. The principle of second-order transfinite recursion STR is equivalent over GBC to the second-order comprehension principle. In other words, GBC+STR is equivalent to KM.

Proof. Kelley-Morse set theory proves that every second-order recursion has a solution in the same way that ZFC proves that every set-length well-ordered recursion has a solution. Namely, we simply consider the classes which are partial solutions to the recursion, in that they obey the recursive requirement, but possibly only on an initial segment of the well-order $\Gamma$. We may easily show by induction that any two such partial solutions agree on their common domain (this uses second-order comprehension in order to find the least point of disagreement, if any), and we can show that any given partial solution, if not already a full solution, can be extended to a partial solution on a strictly longer initial segment. Finally, we show that the common values of all partial solutions is therefore a solution of the recursion. This final step uses second-order comprehension in order to define what the common values are for the partial solutions to the recursion.

Conversely, the principle of second-order transfinite recursion clearly implies the second-order comprehension axiom, by considering recursions of length one. For any second-order assertion $\varphi$ and class parameter $Z$, we may deduce that $\{x\mid \varphi(x,Z)\}$ is a class, and so the second-order class comprehension principle holds. $\Box$

It is natural to consider various fragments of STR, such as $\Sigma^1_n\text{-}\text{TR}_\Gamma$, which is the assertion that every $\Sigma^1_n$-formula $\varphi$ admits a solution for recursions of length $\Gamma$.  Such principles are provable in proper fragments of KM, since for a given level of complexity, we only need a corresponding fragment of comprehension to undertake the proof that the recursion has a solution. The full STR asserts $\Sigma^1_\omega\text{-}\text{TR}$, allowing any length. The theorem shows that STR is equivalent to recursions of length $1$, since once you get the second-order comprehension principle, then you get solutions for recursions of any length. Thus, with second-order transfinite recursion, a little goes a long way. Perhaps it is more natural to think of transfinite recursion in this context not as axiomatizing KM, since it clearly implies second-order comprehension straight away, but rather as an apparent strengthening of KM that is actually provable in KM. This contrasts with the first-order situation of ETR with respect to GBC, where GBC+ETR does make a proper strengthening of GBC.

• V. Gitman and J. D. Hamkins, “Open determinacy for class games,” in Foundations of Mathematics, Logic at Harvard, Essays in Honor of Hugh Woodin’s 60th Birthday, A. E. Caicedo, J. Cummings, P. Koellner, and P. Larson, Eds., American Mathematical Society, 2016. (also available as Newton Institute preprint ni15064)
@INCOLLECTION{GitmanHamkins2016:OpenDeterminacyForClassGames,
author = {Victoria Gitman and Joel David Hamkins},
title = {Open determinacy for class games},
booktitle = {Foundations of Mathematics, Logic at Harvard, Essays in Honor of Hugh Woodin's 60th Birthday},
publisher = {American Mathematical Society},
year = {2016},
editor = {Andr\'es E. Caicedo and James Cummings and Peter Koellner and Paul Larson},
volume = {},
number = {},
series = {Contemporary Mathematics},
type = {},
chapter = {},
pages = {},
edition = {},
month = {},
note = {also available as Newton Institute preprint ni15064},
url = {http://jdh.hamkins.org/open-determinacy-for-class-games},
eprint = {1509.01099},
archivePrefix = {arXiv},
primaryClass = {math.LO},
abstract = {},
keywords = {},
}

• V. Gitman, J. D. Hamkins, P. Holy, P. Schlicht, and K. Williams, “The exact strength of the class forcing theorem,” ArXiv e-prints, 2017. (manuscript under review)
@ARTICLE{GitmanHamkinsHolySchlichtWilliams:The-exact-strength-of-the-class-forcing-theorem,
author = {Victoria Gitman and Joel David Hamkins and Peter Holy and Philipp Schlicht and Kameryn Williams},
title = {The exact strength of the class forcing theorem},
journal = {ArXiv e-prints},
year = 2017,
month = jul,
volume = {},
number = {},
pages = {},
note = {manuscript under review},
abstract = {},
keywords = {},
source = {},
doi = {},
eprint = {1707.03700},
archivePrefix = {arXiv},
primaryClass = {math.LO},
url = {http://jdh.hamkins.org/class-forcing-theorem},
}

Photo by Petar Milošević (Own work) [CC BY-SA 4.0], via Wikimedia Commons

The exact strength of the class forcing theorem

• V. Gitman, J. D. Hamkins, P. Holy, P. Schlicht, and K. Williams, “The exact strength of the class forcing theorem,” ArXiv e-prints, 2017. (manuscript under review)
@ARTICLE{GitmanHamkinsHolySchlichtWilliams:The-exact-strength-of-the-class-forcing-theorem,
author = {Victoria Gitman and Joel David Hamkins and Peter Holy and Philipp Schlicht and Kameryn Williams},
title = {The exact strength of the class forcing theorem},
journal = {ArXiv e-prints},
year = 2017,
month = jul,
volume = {},
number = {},
pages = {},
note = {manuscript under review},
abstract = {},
keywords = {},
source = {},
doi = {},
eprint = {1707.03700},
archivePrefix = {arXiv},
primaryClass = {math.LO},
url = {http://jdh.hamkins.org/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).

• V. Gitman, J. D. Hamkins, P. Holy, P. Schlicht, and K. Williams, “The exact strength of the class forcing theorem,” ArXiv e-prints, 2017. (manuscript under review)
@ARTICLE{GitmanHamkinsHolySchlichtWilliams:The-exact-strength-of-the-class-forcing-theorem,
author = {Victoria Gitman and Joel David Hamkins and Peter Holy and Philipp Schlicht and Kameryn Williams},
title = {The exact strength of the class forcing theorem},
journal = {ArXiv e-prints},
year = 2017,
month = jul,
volume = {},
number = {},
pages = {},
note = {manuscript under review},
abstract = {},
keywords = {},
source = {},
doi = {},
eprint = {1707.03700},
archivePrefix = {arXiv},
primaryClass = {math.LO},
url = {http://jdh.hamkins.org/class-forcing-theorem},
}

Open and clopen determinacy for proper class games, VCU MAMLS April 2017

This will be a talk for the Mid-Atlantic Mathematical Logic Seminar at Virginia Commonwealth University, a conference to be held April 1-2, 2017.

Abstract. The principle of open determinacy for class games — two-player games of perfect information with plays of length $\omega$, where the moves are chosen from a possibly proper class, such as games on the ordinals — is not provable in Zermelo-Fraenkel set theory ZFC or Gödel-Bernays set theory GBC, if these theories are consistent, because provably in ZFC there is a definable open proper class game with no definable winning strategy. In fact, the principle of open determinacy and even merely clopen determinacy for class games implies Con(ZFC) and iterated instances Con(Con(ZFC)) and more, because it implies that there is a satisfaction class for first-order truth, and indeed a transfinite tower of truth predicates $\text{Tr}_\alpha$ for iterated truth-about-truth, relative to any class parameter. This is perhaps explained, in light of the Tarskian recursive definition of truth, by the more general fact that the principle of clopen determinacy is exactly equivalent over GBC to the principle of elementary transfinite recursion ETR over well-founded class relations. Meanwhile, the principle of open determinacy for class games is provable in the stronger theory GBC+$\Pi^1_1$-comprehension, a proper fragment of Kelley-Morse set theory KM. New work by Hachtman and Sato, respectively has clarified the separation of clopen and open determinacy for class games.

This is joint work with Victoria Gitman. See our article, Open determinacy for class games.

Slides