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”]

Kameryn J. Williams, PhD 2018, CUNY Graduate Center

Kameryn J. Williams successfully defended his dissertation under my supervision at the CUNY Graduate Center on April 6th, 2018, earning his Ph.D. degree in May 2018. He has accepted a position in mathematics at the University of Hawaii, to begin Fall 2018.

What a pleasure it was to work with Kameryn, an extremely talented mathematician with wide interests and huge promise.

Kameryn J Williams | MathOverflow | ar$\chi$iv

Kameryn J. Williams, The Structure of Models of Second-order Set Theories,  Ph.D. dissertation for The Graduate Center of the City University of New York, May, 2018. arXiv:1804.09526.

Abstract. This dissertation is a contribution to the project of second-order set theory, which has seen a revival in recent years. The approach is to understand second-order set theory by studying the structure of models of second-order set theories. The main results are the following, organized by chapter. First, I investigate the poset of T-realizations of a fixed countable model of ZFC, where T is a reasonable second-order set theory such as GBC or KM, showing that it has a rich structure. In particular, every countable partial order embeds into this structure. Moreover, we can arrange so that these embedding preserve the existence/nonexistence of upper bounds, at least for finite partial orders. Second I generalize some constructions of Marek and Mostowski from KM to weaker theories. They showed that every model of KM plus the Class Collection schema “unrolls” to a model of ZFC− with a largest cardinal. I calculate the theories of the unrolling for a variety of second-order set theories, going as weak as GBC + ETR. I also show that being T-realizable goes down to submodels for a broad selection of second-order set theories T. Third, I show that there is a hierarchy of transfinite recursion principles ranging in strength from GBC to KM. This hierarchy is ordered first by the complexity of the properties allowed in the recursions and second by the allowed heights of the recurions. Fourth, I investigate the question of which second-order set theories have least models. I show that strong theories—such as KM or $\Pi^1_1$-CA—do not have least transitive models, while weaker theories—from GBC to GBC + ETR${}_{\text{Ord}}$—do have least transitive models.

In addition to his dissertation work and the research currently arising out of it, Kameryn has undertaken a number of collaborations with various international research efforts, including the following:

  • He is a co-author on The exact strength of the class forcing theorem. [bibtex key=”GitmanHamkinsHolySchlichtWilliams:The-exact-strength-of-the-class-forcing-theorem”]
  • He is co-author on a current joint project with Miha Habič, myself, Daniel Klausner and Jonathan Verner concerning the nonamalgamation phenomenon in the generic multiverse of a countable model of set theory.
  • He is co-author on a current joint project with myself and Philip Welch concerning the universal $\Sigma_1$-definable finite sequence, an analogue of the universal finite set, but for the constructible universe.

 

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