Recursively saturated and rather classless

A mathematics blog by Kameryn Williams

Category: Class Forcing

The structure of models of second-order set theories

This is my PhD dissertation.

[PDF] [PDF (single spaced)] [arXiv] [CUNY Academic Works (forthcoming)] [bibTeX]

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 recursions. 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 + ETROrd—do have least transitive models.

fig4.4


Bibtex

@PHDTHESIS{Williams:dissertation,
author = {Kameryn J Williams},
title = {The structure of models of second-order set theories},
school = {The Graduate Center, The City University of New York},
year = {2018},
eprint = {1804.09526},
archivePrefix ={arXiv},
primaryClass = {math.LO},
url = {https://kamerynblog.wordpress.com/2018/04/25/the-structure-of-models-of-second-order-set-theories},
}

Advertisements

Forcing classes to have the same size

Work in second-order set theory. If Global Choice holds, then all proper classes have the same size. There is a bijection between V and \mathrm{Ord} so by restricting that bijection to A \subseteq V we get a bijection between A and a proper-class sized subclass of \mathrm{Ord}, which is of course in bijection with \mathrm{Ord}. But if Global Choice fails then there can be classes of different size. For example, consider an inaccessible cardinal \kappa so that V_\kappa does not have a definable global well-order. Then V_\kappa equipped with its definable subsets as classes gives a model of Gödel–Bernays set theory (without Global Choice) whose \mathrm{Ord} (= \kappa) is not in bijective correspondence with its V (= V_\kappa).

Suppose we start out with Global Choice failing, and hence there being classes of different size. What happens if we try to force classes to have the same size?

Let’s start with a warm-up.

Proposition: Work in \mathsf{GB}^-, i.e. Gödel–Bernays set theory with neither Global Choice nor Powerset. If C \subseteq \mathrm{Ord}^M is generic for the forcing to add a Cohen-generic subclass of \mathrm{Ord}, then from C can be defined (in a first-order way) a global well-order of ordertype \mathrm{Ord}. In particular, all classes have the same size in the Cohen-extension.

Some remarks before the proof. First, to be clear, the Cohen poclass consists of set-sized partial functions from \mathrm{Ord} to 2, ordered by reverse inclusion. Second, in the absence of Powerset the various formulations of Global Choice are not equivalent. The version obtained from a Cohen-generic subclass of \mathrm{Ord} is the strongest. Having a global well-order of ordertype \mathrm{Ord} (equivalently, having a bijection from \mathrm{Ord} to V) is stronger than having a global well-order (of any ordertype), stronger than cardinal comparability for classes, and stronger than the existence of a global choice function. Whereas with Powerset they are all equivalent.

Proof: Every set is coded as a set of ordinals. This is because we can code a set x by taking an isomorphic copy of \mathord{\in} \upharpoonright \mathrm{TC}(\{x\}) as a set of pairs of ordinals. Since we have a definable pairing function for ordinals, we can code a set of pairs of ordinals as a set of ordinals. Now observe that by genericity every set of ordinals is coded into a Cohen-generic subclass of \mathrm{Ord}: if p is a condition in the forcing then extend p by adding a copy of (the characteristic function for) the set of ordinals starting above \sup \mathrm{dom}(p). So we can define a global well-order of order-type \mathrm{Ord} by saying that x < y if the first place in the generic C where x is coded comes before the first place in the generic where y is coded. ∎

The upshot of this proposition is that once you add a Cohen-generic subclass of \mathrm{Ord}, you’ve forced every class to have the same size. So if you want classes of different sizes you cannot add Cohen-generic subclasses of \mathrm{Ord}.

Let’s consider a more direct way to force two classes to have the same size. Let X and Y be proper classes. Define the partially-ordered class \mathbb B(X,Y) to consist of all set-sized partial injections from X to Y, ordered by reverse inclusion. By genericity, if B is generic for \mathbb B(X,Y) then every member of X is in its domain and every member of Y is in its range. So B will be a bijection between X and Y, forcing them to have the same size.

Before saying something about this \mathbb B(X,Y) forcing, I need a definition.

Definition: A proper class A is amorphous if there is no way to decompose A into a disjoint union of two proper classes.

This is modeled upon the definition of an amorphous set, i.e. an infinite set which cannot be decomposed into a disjoint union of two infinite sets. (Of course, a fragment of choice rules out the existence of amorphous sets.) Indeed, we can get models with amorphous classes by considering amorphous sets. Work in a universe with amorphous subsets of H_{\omega_1}. Then, (H_{\omega_1}, \mathcal P(H_{\omega_1})) is a model of \mathsf{GB}^- - \mathrm{Choice} which has amorphous classes.

Proposition: Suppose that the proper class Y is not amorphous. Then forcing with \mathbb B(\mathrm{Ord},Y) adds a Cohen-generic subclass of \mathrm{Ord}. Put as a slogan: forcing a non-amorphous class to be the same size as \mathrm{Ord} forces all classes to have the same size.

Proof: Let Y_0 and Y_1 be disjoint proper classes whose union is Y. We will use them to extract a Cohen-generic subclass of \mathrm{Ord} from a generic B for \mathbb B(\mathrm{Ord},Y). Specifically, define a function C : \mathrm{Ord} \to 2 as C(\alpha) = i iff B(\alpha) \in Y_i. More generally, any condition b \in \mathbb B(\mathrm{Ord},Y) defines a condition p(b) in the Cohen poclass; namely for \alpha \in \mathrm{dom}(b) define p(b)(\alpha) = i iff b(\alpha) \in Y_i. Because Y_0 and Y_1 are both proper classes this map b \mapsto p(b) is onto the Cohen poclass.

Let us see that this C is Cohen-generic. Take any dense subclass D of the Cohen poclass. Let D' = \{ b \in \mathbb B(\mathrm{Ord},Y) : \exists p \in D\ p = p(b) \}. This D' is a dense subclass of \mathbb B(\mathrm{Ord},Y). Otherwise, there would be b \in \mathbb B(\mathrm{Ord},Y) with no extension in D'. But then p(b) would have no extension in D, contradicting the density of D. Thus, since B meets D', we get that C meets D. As D was arbitrary, C is generic for the Cohen poclass. ∎

We can generalize this result. Instead of considering the class \mathrm{Ord} we can consider any class X \supseteq \mathrm{Ord}. We then work similarly, but define p(b) by first restricting b to \mathrm{Ord} and then checking whether b(\alpha) is in Y_0 or Y_1. And it clearly doesn’t matter which coordinate is first or second. So forcing with \mathbb B(X,Y) for either X \supseteq \mathrm{Ord} or Y \supseteq \mathrm{Ord} (and both non-amorphous) forces all classes to have the same size.

In summary, for a large collection of classes we would like to force to have the same size, doing so via the obvious poclass has the effect of making all classes have the same size. Does this always happen, even if neither class contains \mathrm{Ord}?

Question: Over \mathsf{GB}^-, must \mathbb B(X,Y) always force all classes to have the same size?

I’m not 100% clear on the role of amorphous classes here. I needed that my classes were not amorphous, but I suspect that this comes for free in my context. I strongly suspect the following question has a positive answer, but don’t have the choiceless set theory know-how to easily see a proof.

Question: Does \mathsf{GB}^- prove that there are no amorphous classes? That is, does having the axiom of choice for sets imply there are no amorphous classes?

A positive answer would be analogous to the ZF fact that countable choice implies there are no amorphous sets.

The exact strength of the class forcing theorem

This will be a talk at CUNY Set Theory Seminar on Friday, October 13.

Slides.

Gödel–Bernays set theory \mathsf{GBC} proves that sufficiently nice (i.e. pretame) class forcings satisfy the forcing theorem—that is, these forcing relations \mathbb P admit forcing relations \Vdash_\mathbb{P} satisfying the recursive definition of the forcing relation. It follows that statements true in the corresponding forcing extensions are forced and forced statements are true. But there are class forcings for which having their forcing relation exceeds \mathsf{GBC} in consistency strength. So \mathsf{GBC} does not prove the forcing theorem for all class forcings. This is in contrast to the well-known case of set forcing, where \mathsf{ZFC} proves the forcing theorem for all set forcings. On the other hand, stronger second-order set theories such as Kelley–Morse set theory \mathsf{KM} prove the forcing theorem for all class forcings, providing an upper bound. What is the exact strength of the class forcing theorem?

I will show that, over \mathsf{GBC}, the forcing theorem for all class forcings is equivalent to \mathsf{ETR}_\mathrm{Ord} the principle of elementary transfinite recursion for recursions of height \mathrm{Ord}. This is equivalent to the existence of \mathrm{Ord}-iterated truth predicates for first-order truth relative to any class parameter; which is in turn equivalent to the existence of truth predicates for the infinitary languages \mathcal L_{\mathrm{Ord}, \omega}(\in, A) allowing any class parameter A. This situates the class forcing theorem precisely in the hierarchy of theories between \mathsf{GBC} and \mathsf{KM}.

This is joint work with Victoria Gitman, Joel Hamkins, Peter Holy, and Philipp Schlict from our paper of the same name.

ClassForcing

The exact strength of the class forcing theorem

This will be a talk at the Kurt Gödel Research Center Research Seminar on Tuesday, September 26. See also their page for the talk. Slides here.

Gödel–Bernays set theory \mathsf{GBC} proves that sufficiently nice (i.e. pretame) class forcings satisfy the forcing theorem—that is, these forcing relations \mathbb P admit forcing relations \Vdash_\mathbb{P} satisfying the recursive definition of the forcing relation. It follows that statements true in the corresponding forcing extensions are forced and forced statements are true. But there are class forcings for which having their forcing relation exceeds \mathsf{GBC} in consistency strength. So \mathsf{GBC} does not prove the forcing theorem for all class forcings. This is in contrast to the well-known case of set forcing, where \mathsf{ZFC} proves the forcing theorem for all set forcings. On the other hand, stronger second-order set theories such as Kelley–Morse set theory \mathsf{KM} prove the forcing theorem for all class forcings, providing an upper bound. What is the exact strength of the class forcing theorem?

I will show that, over \mathsf{GBC}, the forcing theorem for all class forcings is equivalent to \mathsf{ETR}_\mathrm{Ord} the principle of elementary transfinite recursion for recursions of height \mathrm{Ord}. This is equivalent to the existence of \mathrm{Ord}-iterated truth predicates for first-order truth relative to any class parameter; which is in turn equivalent to the existence of truth predicates for the infinitary languages \mathcal L_{\mathrm{Ord}, \omega}(\in, A) allowing any class parameter A. This situates the class forcing theorem precisely in the hierarchy of theories between \mathsf{GBC} and \mathsf{KM}.

This is joint work with Victoria Gitman, Joel Hamkins, Peter Holy, and Philipp Schlict from our paper of the same name.

ClassForcing

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”. (under review) arXiv bibTeX

Abstract The class forcing theorem, which asserts that every class forcing notion \mathbb P admits a forcing relation \Vdash_{\mathbb 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 \mathsf{GBC} to the principle of elementary transfinite recursion \mathsf{ETR}_{\mathrm{Ord}} for class recursions of length \mathrm{Ord}. It is also equivalent to the existence of truth predicates for the infinitary languages \mathcal{L}_{\mathrm{Ord},\omega}(\in,A), allowing any class parameter A; to the existence of truth predicates for the language \mathcal{L}_{\mathrm{Ord},\mathrm{Ord}}(\in,A); to the existence of \mathrm{Ord}-iterated truth predicates for first-order set theory \mathcal{L}_{\omega,\omega}(\in,A); to the assertion that every separative class partial order \mathbb 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 \mathrm{Ord}+1. Unlike set forcing, if every class forcing notion \mathbb P has a forcing relation merely for atomic formulas, then every such \mathbb 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 \mathsf{GBC} and Kelley-Morse set theory \mathsf{KM}.

We shall characterize the exact strength of the class forcing theorem, which asserts that every class forcing notion \mathbb{P} has a corresponding forcing relation \Vdash_\mathbb{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 set forcing, for which one may prove in \mathsf{ZFC} that every set forcing notion has corresponding forcing relations, with class forcing it is consistent with Gödel-Bernays set theory \mathsf{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 \mathrm{Con}(\mathsf{ZFC}) and much more, and so the consistency strength of the class forcing theorem strictly exceeds \mathsf{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 \mathsf{GBC} and \mathsf{KM}. It turns out that the class forcing theorem is equivalent over \mathsf{GBC} to an attractive collection of several other natural set-theoretic assertions; it is a robust axiomatic principle.

ClassForcing.png

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 \mathsf{GBC} and \mathsf{KM} and beyond, analyzing the strength of various assertions in second-order set theory, such as the principle \mathsf{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 \mathsf{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 formulae p\Vdash\sigma=\tau and p\Vdash\sigma\in\tau.
  2. The class forcing theorem schema: 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 subformulae p\Vdash\varphi(\vec \tau,\dot\Gamma_0,\ldots,\dot\Gamma_m).
  3. The uniform first-order class forcing theorem: every class forcing notion \mathbb{P} admits a uniform forcing relation p\Vdash\varphi(\vec \tau,\dot\Gamma_0,\ldots,\dot\Gamma_m) applicable to all assertions \varphi\in\mathcal{L}_{\omega,\omega}(\in,V^\mathbb{P},\dot\Gamma_0,\ldots,\dot\Gamma_m) in the first-order forcing language with finitely many class names.
  4. The uniform infinitary class forcing theorem: every class forcing notion \mathbb{P} admits a uniform forcing relation p\Vdash\varphi(\vec \tau,\dot\Gamma_0,\ldots,\dot\Gamma_m) applicable to all assertions \varphi\in\mathcal{L}_{\mathrm{Ord},\mathrm{Ord}}(\in,V^\mathbb{P},\dot\Gamma_0,\ldots,\dot\Gamma_m) in the infinitary forcing language with finitely many class names.
  5. Names for truth predicates: every class forcing notion \mathbb{P} has a class name \dot T and a forcing relation for which \mathbf{1}\Vdash\dot T is a truth-predicate for the first-order forcing language with finitely many class names \mathcal{L}_{\omega,\omega}(\in,V^\mathbb{P},\dot\Gamma_0,\ldots,\dot\Gamma_m).
  6. Boolean completions: Every class forcing notion \mathbb{P}, that is, every separative class partial order, admits a Boolean completion \mathbb B, a set-complete class Boolean algebra into which \mathbb{P} densely embeds.
  7. The class-join separation principle plus \mathsf{ETR}_{\mathrm{Ord}}-foundation.
  8. For every class A, there is a truth predicate for \mathcal{L}_{\mathrm{Ord},\omega}(\in,A).
  9. For every class A, there is a truth predicate for \mathcal{L}_{\mathrm{Ord},\mathrm{Ord}}(\in,A).
  10. For every class A, there is an \mathrm{Ord}-iterated truth predicate for \mathcal{L}_{\omega,\omega}(\in,A).
  11. The principle of determinacy for clopen class games of rank at most \mathrm{Ord}+1.
  12. The principle \mathsf{ETR}_{\mathrm{Ord}} of elementary transfinite recursion for \mathrm{Ord}-length recursions of first-order properties, using any class parameter.

Bibtex

@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 = {},
year = {},
volume = {},
number = {},
pages = {},
month = {},
note = {manuscript under review},
abstract = {},
keywords = {},
source = {},
doi = {},
eprint = {1707.03700},
archivePrefix = {arXiv},
primaryClass = {math.LO},
url = {http://jdh.hamkins.org/class-forcing-theorem},
}

Usually well-behaved class forcings can behave quite badly in the absence of choice

I recently stumbled upon yet another example of how class forcing can be wilder than set forcing. A class forcing can be well-behaved under the assumption that the ground model satisfies the axiom of choice while being destructive if choice fails in the ground model. (Thank you to Joel David Hamkins for a helpful conversation and for noticing the key fact I had missed.)

Proposition: There is a (definable) class forcing \mathbb G so that:

  1. If (M,\mathcal X) \models \mathsf{GB} + \mathsf{AC} then forcing with \mathbb G^M over (M,\mathcal X) preserves \mathsf{GB} + \mathsf{AC}.
  2. If (M,\mathcal X) \models \mathsf{GB} + \neg \mathsf{AC} then forcing with \mathbb G^M over (M,\mathcal X) does not preserve Replacement.

Proof: This forcing \mathbb G is the forcing to add a global choice function. Specifically, conditions in \mathbb G are functions g : \alpha \to V whose domains are ordinals. The order is the natural one, namely g \le h if g extends h. (Observe that this definition only depends upon the first-order part of our model of set theory, justifying the use of \mathbb G^M above instead of \mathbb G^{(M,\mathcal X)}.)

An easy density argument shows that for any a \in V it is dense to get a in the range of a condition. Therefore, forcing with \mathbb G adds a surjection G : \mathrm{Ord} \to V, from which we can easily define a global choice function. Note that this doesn’t require the ground model to satisfy any fragment of choice. While we will see that forcing with \mathbb G over a model without choice kills Replacement, at least we get Global Choice as a consolation prize.

We also have that \mathbb G is \mathord<\mathrm{Ord}-closed, meaning that any set-sized decreasing sequence of conditions has a lower bound. Given a descending sequence \langle g_\xi : \xi < \alpha \rangle of conditions from \mathbb G, they have \bigcup_{\xi < \alpha} g_\xi as a lower bound. Therefore, forcing with \mathbb G does not add any new sets. In particular, if we start with a model of \mathsf{AC}, then choice is preserved.

To finish the argument for (1) of the Proposition we need to see that \mathsf{GB} is preserved. For that, I will be lazy and link to a pair [1, 2] of blog posts by Victoria Gitman who was kind enough to write up the gritty details. Let’s check, however, where  Vika’s argument uses that choice holds in the ground model. Consider her argument that Replacement is preserved, i.e. that if F is a class (in the forcing extension) and a is a set then F \upharpoonright a is a set. Vika does this by contradiction, assuming some g in the generic forces \dot F \upharpoonright \check a. She then finds a stronger  condition which decides \dot F \upharpoonright \check a, leading to the desired contradiction. To do this, she uses a well-order of a. Of course, if choice fails, then we can find a with no well-order, so her argument won’t work in that context.

Now let’s see (2) of the Proposition. Suppose we have a ground model set which lacks a well-order. Call this set b. As we saw above, if G is the generic function \mathrm{Ord} \to V added by forcing with \mathbb G, then every element of b appears in the range of G. However, it cannot be that they all appear by some bounded stage. If it were that b \subseteq \mathrm{ran}(G \upharpoonright \alpha) for some ordinal \alpha, then since G \upharpoonright \alpha is a set from the ground model, we would have a well-order of b in the ground model, contrary to our assumption.

This gives a failure of Replacement. Namely, consider the function F taking a \in V to the least \alpha so that G(\alpha) = a. By the above paragraph, we get that F '' b \subseteq_{\mathsf{cof}} \mathrm{Ord} is not a set.

The following corollary can be extracted from the above argument.

Corollary: In the absence of Replacement, Global Choice does not imply (Set) Choice. In other words, in the absence of Replacement the existence of a (class) function which picks elements from every nonempty set does not imply the existence of a set function which picks elements from every nonempty subset of a set b.

I view this corollary as (yet more) evidence of the importance of Replacement. It is necessary to prove the ‘obvious fact’ that Global Choice implies (Set) Choice.