Determinacy for proper class games, Seminaire de Logique Lyon-Paris, April 2021

This will be a talk for the Seminaire de Logique Lyon-Paris on 14 April 2021 4pm Paris time (3pm UK). The talk will be held on Zoom at
875 1148 7359
.

Abstract. The principle of open determinacy for class games — two-player games of perfect information with plays of length ω, 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 strictly stronger, although it is provable in the stronger theory GBC+$\Pi^1_1$-comprehension, a proper fragment of Kelley-Morse set theory KM.

Open class determinacy is preserved by forcing

[bibtex key=”HamkinsWoodin2018:Open-class-determinacy-is-preserved-by-forcing”]

Abstract. The principle of open class determinacy is preserved by pre-tame class forcing, and after such forcing, every new class well-order is isomorphic to a ground-model class well-order. Similarly, the principle of elementary transfinite recursion ETR${}_\Gamma$ for a fixed class well-order $\Gamma$ is preserved by pre-tame class forcing. The full principle ETR itself is preserved by countably strategically closed pre-tame class forcing, and after such forcing, every new class well-order is isomorphic to a ground-model class well-order. Meanwhile, it remains open whether ETR is preserved by all forcing, including the forcing merely to add a Cohen real.

 

The principle of elementary transfinite recursion ETR — according to which every first-order class recursion along any well-founded class relation has a solution — has emerged as a central organizing concept in the hierarchy of second-order set theories from Gödel-Bernays set theory GBC up to Kelley-Morse set theory KM and beyond. Many of the principles in the hierarchy can be seen as asserting that certain class recursions have solutions.

In addition, many of these principles, including ETR and its variants, are equivalently characterized as determinacy principles for certain kinds of class games. Thus, the hierarchy is also fruitfully unified and organized by determinacy ideas.

This hierarchy of theories is the main focus of study in the reverse mathematics of second-order set theory, an emerging subject aiming to discover the precise axiomatic principles required for various arguments and results in second-order set theory. The principle ETR itself, for example, is equivalent over GBC to the principle of clopen determinacy for class games and also to the existence of iterated elementary truth predicates (see Open determinacy for class games); since every clopen game is also an open game, the principle ETR is naturally strengthened by the principle of open determinacy for class games, and this is a strictly stronger principle (see Hachtman and Sato); the weaker principle ETR${}_\text{Ord}$, meanwhile, asserting solutions to class recursions of length Ord, is equivalent to the class forcing theorem, which asserts that every class forcing notion admits a forcing relation, to the existence of set-complete Boolean completions of any class partial order, to the existence of Ord-iterated elementary truth predicates, to the determinacy of clopen games of rank at most Ord+1, and to other natural set-theoretic principles (see The exact strength of the class forcing theorem).

Since one naturally seeks in any subject to understand how one’s fundamental principles and tools interact, we should like in this article to consider how these second-order set-theoretic principles are affected by forcing. These questions originated in previous work of Victoria Gitman and myself, and question 1 also appears in the dissertation of Kameryn Williams, which was focused on the structure of models of second-order set theories.

It is well-known, of course, that ZFC, GBC, and KM are preserved by set forcing and by tame class forcing, and this is true for other theories in the hierarchy, such as GBC$+\Pi^1_n$-comprehension and higher levels of the second-order comprehension axiom. The corresponding forcing preservation theorem for ETR and for open class determinacy, however, has not been known.

Question 1. Is ETR preserved by forcing?

Question 2. Is open class determinacy preserved by forcing?

We intend to ask in each case about class forcing as well as set forcing. Question 1 is closely connected with the question of whether forcing can create new class well-order order types, longer than any class well-order in the ground model. Specifically, Victoria Gitman and I had observed earlier that ETR${}_\Gamma$ for a specific class well-order $\Gamma$ is preserved by pre-tame class forcing, and this would imply that the full principle ETR would also be preserved, if no fundamentally new class well-orders are created by the forcing. In light of the fact that forcing over models of ZFC adds no new ordinals, that would seem reasonable, but proof is elusive, and the question remains open. Can forcing add new class well-orders, perhaps very tall ones that are not isomorphic to any ground model class well-order? Perhaps there are some very strange models of GBC that gain new class well-order order types in a forcing extension.

Question 3. Assume GBC. After forcing, must every new class well-order be isomorphic to a ground-model class well-order? Does ETR imply this?

The main theorem of this article provides a full affirmative answer to question 2, and partial affirmative answers to questions 2 and 3.

Main Theorem.

  1. Open class determinacy is preserved by pre-tame class forcing. After such forcing, every new class well-order is isomorphic to a ground-model class well-order.
  2. The principle ETR${}_\Gamma$, for any fixed class well order $\Gamma$, is preserved by pre-tame class forcing.
  3. The full principle ETR is preserved by countably strategically closed pre-tame class forcing. After such forcing, every new class well-order is isomorphic to a ground-model class well-order.

We should like specifically to highlight the fact that questions 1 and 3 remain open even in the case of the forcing to add a Cohen real. Is ETR preserved by the forcing to add a Cohen real? After adding a Cohen real, is every new class well-order isomorphic to a ground-model class well-order? One naturally expects affirmative answers, especially in a model of ETR.

For more, click through the arxiv for a pdf of the full article.

[bibtex key=”HamkinsWoodin2018:Open-class-determinacy-is-preserved-by-forcing”]

Determinacy for open class games is preserved by forcing, CUNY Set Theory Seminar, April 2018

This will be a talk for the CUNY Set Theory Seminar, April 27, 2018, GC Room 6417, 10-11:45am (please note corrected date).

Abstract. Open class determinacy is the principle of second order set theory asserting of every two-player game of perfect information, with plays coming from a (possibly proper) class $X$ and the winning condition determined by an open subclass of $X^\omega$, that one of the players has a winning strategy. This principle finds itself about midway up the hierarchy of second-order set theories between Gödel-Bernays set theory and Kelley-Morse, a bit stronger than the principle of elementary transfinite recursion ETR, which is equivalent to clopen determinacy, but weaker than GBC+$\Pi^1_1$-comprehension. In this talk, I’ll given an account of my recent joint work with W. Hugh Woodin, proving that open class determinacy is preserved by forcing. A central part of the proof is to show that in any forcing extension of a model of open class determinacy, every well-founded class relation in the extension is ranked by a ground model well-order relation. This work therefore fits into the emerging focus in set theory on the interaction of fundamental principles of second-order set theory with fundamental set theoretic tools, such as forcing. It remains open whether clopen determinacy or equivalently ETR is preserved by set forcing, even in the case of the forcing merely to add a Cohen real.

On the strengths of the class forcing theorem and clopen class game determinacy, Prague set theory seminar, January 2018

This will be a talk for the Prague set theory seminar, January 24, 11:00 am to about 2pm (!).

Abstract. The class forcing theorem is the assertion that every class forcing notion admits corresponding forcing relations. This assertion is not provable in Zermelo-Fraenkel ZFC set theory or Gödel-Bernays GBC set theory, if these theories are consistent, but it is provable in stronger second-order set theories, such as Kelley-Morse KM set theory. In this talk, I shall discuss the exact strength of this theorem, which turns out to be equivalent to the principle of elementary transfinite recursion ETRord for class recursions on the ordinals. The principle of clopen determinacy for class games, in contrast, is strictly stronger, equivalent over GBC to the full principle of ETR for class recursions over arbitrary class well-founded relations. These results and others mark the beginnings of the emerging subject I call the reverse mathematics of second-order set theory.

The exact strength of the class forcing theorem | Open determinacy for class games

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

This was 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.

Hierarchy between GBC and KM

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.

Slides

https://plus.google.com/u/0/+JoelDavidHamkins1/posts/ekgdakenadv

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

1167px-Wooden_spiral_stairs_(Nebotičnik,_Ljubljana)_croped
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.

  1. [bibtex key=”GitmanHamkins2016:OpenDeterminacyForClassGames”]
  2. [bibtex key=”GitmanHamkinsHolySchlichtWilliams:The-exact-strength-of-the-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

[bibtex key=”GitmanHamkinsHolySchlichtWilliams2020:The-exact-strength-of-the-class-forcing-theorem”]

Abstract. The class forcing theorem, which asserts that every class forcing notion $\newcommand\P{\mathbb{P}}\P$ admits a forcing relation $\newcommand\forces{\Vdash}\forces_\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 $\newcommand\Ord{\text{Ord}}\newcommand\ETR{\text{ETR}}\ETR_{\Ord}$ for class recursions of length $\Ord$. It is also equivalent to the existence of truth predicates for the infinitary languages $\mathcal{L}_{\Ord,\omega}(\in,A)$, allowing any class parameter $A$; to the existence of truth predicates for the language $\mathcal{L}_{\Ord,\Ord}(\in,A)$; to the existence of $\Ord$-iterated truth predicates for first-order set theory $\mathcal{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 separation principle; and to the principle of determinacy for clopen class games of rank at most $\Ord+1$. Unlike set forcing, if every class forcing relation $\P$ has a forcing relation merely for atomic formulas, then every such $\P$ has a uniform forcing relation that applies uniformly to all formulas. Our results situate the class forcing theorem in the rich hierarchy of theories between GBC and Kelley-Morse set theory KM.

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.

Hierarchy between GBC and KM

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.

Implication cycle 12

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).

For more, download the paper from the arxiv: [bibtex key=”GitmanHamkinsHolySchlichtWilliams:The-exact-strength-of-the-class-forcing-theorem”]

See also Victoria’s post, Kameryn’s post.

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.

Richmond A line train bridge

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.

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

Slides

 

 

 

VCU MAMLS 2017