Recursively saturated and rather classless

A mathematics blog by Kameryn Williams

Category: Class Forcing

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

Advertisements

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.