Recursively saturated and rather classless

A mathematics blog by Kameryn Williams

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.

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

On the length of iterated full satisfaction classes

This will be a talk at the Warsaw Workshop on Formal Truth Theories on 2017 Sept 29.

In second-order arithmetic, the principle of arithmetical transfinite recursion \mathsf{ATR} asserts that every arithmetical recursive definition iterated transfinitely has a solution. One particular recursive definition of interest is Tarski’s definition of a truth predicate. This definition is carried out over a well-founded tree of rank \omega. We can go further, defining truth about truth via an arithmetical recursion of rank \omega + \omega, truth about truth about truth via an arithmetical recursion of rank \omega \cdot 3, and so on. In general, \mathsf{ATR} implies the existence of an iterated truth predicate of length \alpha for any ordinal \alpha, by way of a recursion over a tree of rank \omega \cdot \alpha.

Consider now a nonstandard model (M,\mathcal X) of \mathsf{ATR}_0 (= \mathsf{ACA}_0 + \mathsf{ATR}). Since M is nonstandard \mathcal X cannot contain the real truth predicate for M, as from it (M,\mathcal X) could define the standard cut of M. Instead, the object which (M,\mathcal X) thinks is the truth predicate for M is an inductive full satisfaction class. This full satisfaction class is not confined to the real formulae as seen from outside, but also decides the truth or falsity of all formulae (in M) of nonstandard length. More generally, for any \Gamma \in \mathcal X which (M,\mathcal X) thinks is a well-order, \mathcal X contains an inductive \Gamma-iterated full satisfaction class.

(M,\mathcal X) thinks that its full satisfaction class is {\em the} unique truth predicate for M. Given two would-be truth predicates (M,\mathcal X) can inductively show that they agree at each level and thus are the same. Similarly, (M,\mathcal X) thinks its \Gamma-iterated full satisfaction class is the unique \Gamma-iterated truth predicate.

Externally to (M,\mathcal X), however, we know that full satisfaction classes, not even inductive full satisfaction classes, have to be unique. Indeed, as Krajewski showed, no countable (nonstandard) M has a unique inductive full satisfaction class. Analogous questions can be asked about iterated full satisfaction classes. It is easy to see they will not be unique for countable models; if S is an inductive full satisfaction class for countable M then a version of Krajewski’s proof applies to (M,S) to show that M admits continuum many 2-iterated full satisfaction classes which extend S. (With some mild assumptions on M and S we can get continuum many inductive 2-iterated full satisfaction classes extending S.)

Uniqueness is out of the question, but we might hope some invariant can be found. If S is an inductive full satisfaction class for M, we can possibly extend it to an inductive 2-iterated full satisfaction class, then an inductive 3-iterated full satisfaction class, and so on until we reach a point that the iterated full satisfaction class is no longer inductive. If S and S' are inductive full satisfaction classes for M, is the length we can iterate them the same? For that matter, is this length well-defined?

The answer to both questions is no.

Theorem: Suppose that countable nonstandard M \models \mathsf{PA} satisfies the \mathcal L_{\mathsf{PA}}-consequences of \mathsf{PA} + “there is an inductive 2-iterated truth predicate”. If M admits an inductive full satisfaction class, then there are S and S' inductive full satisfaction classes for M so that S can be iterated one step further to get an inductive 2-iterated full satisfaction class while S' cannot.

More generally, the iteration length can be anything at all.

Consider countable nonstandard M \models \mathsf{PA} and a < b \in M. Suppose that M satisfies the \mathcal L_\mathsf{PA}-consequences of \mathsf{PA} + “there is an inductive b-iterated truth predicate”. Then, if M admits an inductive a-iterated truth predicate, there are S_a and S_a' inductive a-iterated full satisfaction classes for M so that S_a can be iterated one step further to an inductive (a+1)-iterated full satisfaction class while S_a' cannot.

My original motivation for investigating these questions was in the context of models of set theory, where similar results apply. Suppose M \models \mathsf{ZF} is countable and \omega-nonstandard and satisfies the \mathcal L_\mathsf{ZF}-consequences of \mathsf{ZF} + “there is a strongly amenable 2-iterated truth predicate”. (Being strongly amenable is the set theoretic analogue of being inductive.) Then, if M admits a strongly amenable full satisfaction class, there are S and S' strongly amenable full satisfaction classes for M so that S can be extended to a strongly amenable 2-iterated full satisfaction class while S' cannot. Similar to the arithmetic case, this generalizes to longer iteration lengths.

As a consequence of this, plus the fact that having solutions to any transfinite recursion is equivalent to having solutions for the recursions to construct iterated truth predicates, strongly separating weak fragments of \mathsf{ETR} is only possible with \omega-standard models. Here, \mathsf{ETR} (Elementary Transfinite Recursion) is a set theoretic analogue of \mathsf{ATR}, introduced by Fujimoto. Say that M \models \mathsf{ZF} strongly separates second-order set theories T and S if M satisfies the first-order consequences of S and of T and there is \mathcal T \subseteq \mathcal P(M) so that (M,\mathcal T) \models T but no \mathcal S \subseteq \mathcal P(M) so that (M,\mathcal S) \models S. Intuitively, M strongly separates S and T if M can be made a model of S but cannot be made a model of T, and this is due to something inherently second-order rather than due to some first-order property of M.

For an ordinal \alpha, let \mathsf{ETR}_\alpha denote the principle that elementary transfinite recursions of rank \le \alpha have solutions. If \beta \gg \alpha then \mathsf{ETR}_\beta and \mathsf{ETR}_\alpha can be separated, simply because \mathsf{ETR}_\beta implies \mathrm{Con}(\mathsf{ETR}_\alpha) (over Gödel–Bernays set theory). This separation can be witnessed by an \omega-nonstandard model. However, if countable M strongly separates \mathsf{ETR}_\beta and \mathsf{ETR}_\alpha then M must be \omega-standard. Indeed, \mathsf{ETR}_\beta and \mathsf{ETR}_\alpha are strongly separated by a transitive model of \mathsf{ZF}.

No such phenomenon occurs in arithmetic, as there is only one standard model of arithmetic. We cannot strongly separate the existence of iterated truth predicates of different length with countable models.

Least models of second-order set theories

K. Williams “Least models of second-order set theories” (under review) arXiv PDF bibTeX

Abstract The main theorems of this paper are (1) there is no least transitive model of Kelley–Morse set theory \mathsf{KM} and (2) there is a least \beta-model—that is, a transitive model which is correct about which of its classes are well-founded—of Gödel–Bernays set theory \mathsf{GBC} + Elementary Transfinite Recursion. Along the way I characterize when a countable model of \mathsf{ZFC} has a least \mathsf{GBC}-realization and show that no countable model of \mathsf{ZFC} has a least \mathsf{KM}-realization. I also show that fragments of Elementary Transfinite Recursion have least \beta-models and, for sufficiently weak fragments, least transitive models. These fragments can be separated from each other and from the full principle of Elementary Transfinite Recursion by consistency strength.
The main question left unanswered by this article is whether there is a least transitive model of \mathsf{GBC} + Elementary Transfinite Recursion.

Every set theorist knows there is a least transitive model of \mathsf{ZFC}. What if we want to ask the same question about second-order set theories? Which second-order set theories, if any, have least transitive models? The answer for \mathsf{GBC} follows immediately from the existence of a least transitive model of \mathsf{ZFC}: the least transitive model of \mathsf{GBC} is (L_\alpha, \mathrm{Def}(L_\alpha)) where L_\alpha is the least transitive model of \mathsf{ZFC}. (Indeed, Shepherdson formulated his original argument in terms of \mathsf{GB} (i.e. without Global Choice), rather than in terms of \mathsf{ZFC}.) But this easy argument won’t work for second-order set theories that assert the existence of more classes.

Indeed, no argument will work for sufficiently strong second-order set theories. Take \mathsf{KM}. Allowing for the existence of impredicatively-defined classes means that models of \mathsf{KM} have enough “meta-ordinals” that tools from admissible set theory can be applied. Starting from a model of \mathsf{KM} we can build another model of \mathsf{KM} whose first-order part is the same but whose second-order part sits off to the side, so to speak.

friedman-things

So no (countable) model of \mathsf{ZFC} has a least \mathsf{KM}-realization and thus there cannot be a smallest transitive model of \mathsf{KM}. (Of course, see the actual paper for more than a brief sketch of the argument.)

But \mathsf{KM} is much stronger than \mathsf{GBC} and there are natural theories in the middle. What about those? For \Pi^1_k\text{-}\mathsf{CA} more or less the same argument as the \mathsf{KM} case goes through, getting that they don’t have least transitive models. (But I don’t give a proof of such in this paper; see my forthcoming dissertation for full details.)

So let’s go lower, to the theory \mathsf{ETR}, which is \mathsf{GBC} augmented with the principle of Elementary Transfinite Recursion. Then \mathsf{ETR} is stronger than \mathsf{GBC} because, say, we can construct the Tarskian satisfaction class for first-order formulae via a class recursion of height \omega. But \mathsf{ETR} is strictly weaker than \Pi^1_1\text{-}\mathsf{CA}.

I don’t actually know whether there is a least transitive model of \mathsf{ETR}. (This is the main open question from my paper.) However, I do show that there is a least \beta-model of \mathsf{ETR}. As well, sufficiently weak fragments of \mathsf{ETR}—such as \mathsf{ETR}_{\mathrm{Ord}} which only asserts that elementary transfinite recursions of height \le \mathrm{Ord} have solutions—do have least transitive models. Combined with the results from my joint paper with Gitman, Hamkins, Holy, and Schlict this gives that there is a smallest transitive model of \mathsf{GBC} which satisfies the forcing theorem for all class forcings. I think that’s neat.


Bibtex

@ARTICLE{Williams:least-models,
author = {Kameryn Williams},
title = {Least models of second-order set theories},
journal = {},
year = {},
volume = {},
number = {},
pages = {},
month = {},
note = {manuscript under review},
abstract = {},
keywords = {},
source = {},
doi = {},
eprint = {1709.03955},
archivePrefix = {arXiv},
primaryClass = {math.LO},
url = {https://kamerynblog.wordpress.com/2017/09/12/least-models-of-second-order-set-theories/},
}

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},
}

Weak fragments of ETR have least transitive models

Everyone who’s anyone knows the Shepardson-Cohen result that there is a least transitive model of \mathsf{ZFC}. Of course, we can ask a similar question about other set theories: given a set theory T, is there is a smallest transitive model of T? This question makes sense even when T is a second-order theory, such as \mathsf{GBC} or \mathsf{KM}. A second-order model (M,\mathcal X) is transitive when its set-set and set-class elementhood relations are the true \in.

Theorem (Shepardson). There is a least transitive model of \mathsf{GBC}.

Namely, the least transitive model of \mathsf{GBC} is (L_\alpha, L_{\alpha+1}), where L_\alpha is the least transitive model of \mathsf{ZFC}.

However, if we ask the same question for second-order set theories much stronger than \mathsf{GBC} we get a negative answer.

Theorem (W., not yet published). There is no transitive model of \mathsf{KM} which is contained in all transitive models of \mathsf{KM}.

What happens if we weaken \mathsf{KM}? If we weaken it all the way down to \mathsf{GBC}, then we get the phenomenon of minimal models. If we only weaken it a little bit, say to \Pi^1_k\text{-}\mathsf{CA} for k \ge 2, then we still do not have least transitive models.

What if we weaken it a lot, but not all the way down to \mathsf{GBC}? Or, starting from the other direction, how much can we strengthen \mathsf{GBC} and retain the existence of minimal models?

Of course, this question must be made more precise. We can come up with silly strengthenings of \mathsf{GBC} which do not have least transitive models. Consider the theory consisting of \mathsf{GBC} plus the assertion that there is no definable global well-order. This theory does not have a least transitive model. (A proof of this can be found in my forthcoming paper which also has a proof for the above theorem.)

I don’t want to muck about too much with making this question precise, so for now I will wave my hands and say the word “natural”. Which natural theories intermediate between \mathsf{GBC} and \mathsf{KM} have minimal models?

One natural theory is \mathsf{ETR}, a strengthening of \mathsf{GBC} which also asserts that any transfinite recursion of a first-order property along a well-founded class relation has a solution. (\mathsf{ETR} stands for “elementary transfinite recursion”, à la the arithmetical transfinite recursion axiom from arithmetic.) This theory sits between \mathsf{GBC} and \mathsf{KM} in strength. It’s stronger than \mathsf{GBC} as it proves, for instance, the existence of a truth predicate for first-order formulae. It’s weaker than \mathsf{KM} as it is provable from \Pi^1_1\text{-}\mathsf{CA}.

(For more on \mathsf{ETR}, see Fujimoto’s “Classes and truth in set theory” or Gitman and Hamkins’s “Open determinacy for class games“.)

Is there a least transitive model of \mathsf{ETR}? While I do not have an answer for this, I do have an answer for some fragments of \mathsf{ETR}.

We can weaker \mathsf{ETR} by only requiring that we have solutions for recursions along relations of low rank. If \alpha is an ordinal then \mathsf{ETR}_\alpha asserts that we have solutions for recursions of rank \le \alpha. Similarly, \mathsf{ETR}_\mathrm{Ord} asserts that we have solutions for recursions of rank \le \mathrm{Ord}.

Proposition. If \alpha = \mathrm{Ord} or \alpha < \mathrm{Ord} so that \alpha = \omega \cdot \alpha, then there is a least transitive model of \mathsf{ETR}_\alpha.

In the remainder of this post I want to prove this proposition.

The first step is to reduce \mathsf{ETR} to having solutions just for certain recursions. Gitman and Hamkins showed that \mathsf{ETR} is equivalent to having, for any class well-order \Gamma and any class Z, an iterated truth predicate along \Gamma relative to the class Z. (See their Theorem 8.) Staring at their proof for a few moments, one sees that they showed that whenever \alpha = \omega \cdot \alpha that \mathsf{ETR}_\alpha is equivalent to having iterated truth predicates along \alpha relative to any class Z.

Thus, we can build models of \mathsf{ETR}_\alpha just by ensuring that we have enough iterated truth predicates.

Lemma. Suppose that (M,\mathcal X) \models \mathsf{ETR}_\alpha is transitive and has a global well-order which is first-order definable without any class parameters, where \alpha = \omega \cdot \alpha or \alpha = \mathrm{Ord}. Then M has a smallest \mathsf{ETR}_\alpha-realization. That is, there is \mathcal Y \subseteq \mathcal P(M) so that (M,\mathcal Y) \models \mathsf{ETR}_\alpha and whenever (M,\mathcal Z) \models \mathsf{ETR}_\alpha we have \mathcal Y \subseteq \mathcal Z.

Proof: Let \mathcal Y_0 = \mathrm{Def}(M). Then, (M, \mathcal Y_0) \models \mathsf{GBC}, because M has a definable global well-order. However, (M, \mathcal Y_0) \not \models \mathsf{ETR}_\alpha as it doesn’t even have a truth predicate. Let T_0 be the \alpha-iterated truth predicate for M relative to \emptyset. Then, because T_0 \in \mathcal X, if we set \mathcal Y_1 = \mathrm{Def}(M,T_0) we have (M, \mathcal Y_1) \models \mathsf{GBC}. We still do not have a model of \mathsf{ETR}_\alpha, because \mathcal Y_1 doesn’t contain the \alpha-iterated truth predicate relative to T_0. So let T_1 be this truth predicate and set \mathcal Y_2 = \mathrm{Def}(M,T_1).

Keep going on in this manner. Having defined T_{n-1} and \mathcal Y_n = \mathrm{Def}(M,T_{n-1}), next let T_n be the \alpha-iterated truth predicate relative to T_{n-1} and set \mathcal Y_{n+1} = \mathrm{Def}(M,T_n).

After \omega steps, set \mathcal Y = \bigcup_n \mathcal Y_n. We get that (M,\mathcal Y) \models \mathsf{GBC} because it is the union of an increasing chain of models of \mathsf{GBC}. More, for any class A \in \mathcal Y we have A \in \mathcal Y_n for some n. Hence, \mathcal Y_{n+1} will contain the \alpha-iterated truth predicate for M relative to A. Altogether, this gives that (M,\mathcal Y) \models \mathsf{ETR}_\alpha.

It remains only to see that \mathcal Y is contained in every \mathsf{ETR}_\alpha-realization for M. But this is simply because any (M,\mathcal Z) \models \mathsf{ETR}_\alpha must contain T_n for every n. Since \mathcal Y is the smallest \mathsf{GBC}-realization for M containing all of the T_n, it must be contained within \mathcal Z.

Note that we could have built \mathcal Y in a single step as \mathcal Y = \mathrm{Def}(M; \mathrm{Tr}_\Gamma : \Gamma < \alpha \cdot \omega), i.e. the smallest \mathsf{GBC}-realization for M which contains the \Gamma-iterated truth predicate for M for all \Gamma < \alpha \cdot \omega.

This argument needs that truth predicates for M are unique, which is true for transitive M. On the other hand, \omega-nonstandard models can admit mutually incompatible full satisfaction classes which decide the ‘truth’ of nonstandard formulae in different ways.

This lemma gets us most of the way towards proving the above proposition.

Proof of proposition: Let \eta be the least ordinal \eta' so that L_{\eta'} is \mathsf{ETR}_\alpha-realizable. By the above lemma, L_\eta has a least \mathsf{ETR}_\alpha-realization \mathcal Y. I claim that (L_\eta, \mathcal Y) is the least transitive model of \mathsf{ETR}_\alpha.

To see this, take transitive (M,\mathcal X) \models \mathsf{ETR}_\alpha. There are two cases to consider. The first is if \mathrm{Ord}^M = \eta. We need to see that \mathrm{Tr}^{L_\eta}_\Gamma \in \mathcal X for each \Gamma < \alpha \cdot \omega. This can be seen by noticing that \mathrm{Tr}^{L_\eta}_\Gamma = \{ \phi : \phi^L \in \mathrm{Tr}^M_\Gamma \} and using that \mathrm{Tr}^M_\Gamma \in \mathcal X whenever \Gamma < \alpha \cdot \omega. The second case is if \mathrm{Ord}^M > \eta. In this case, L_\eta \in M, so \mathrm{Tr}^{L_\eta}_\Gamma \in M for \Gamma < \alpha \cdot \omega and thus \mathcal Y \in M.

What if we want to go beyond \mathrm{Ord}? If we are dealing with iterated truth predicates whose length is set-sized, then we have a canonical choice for its length, namely the von Neumann ordinal. But when we look at class-sized well-orders we have to contend with the fact that being well-founded is not absolute for transitive models of second-order set theories. There are transitive models of, say, \mathsf{KM} or \mathsf{ETR} which contain class relations the model wrongly thinks is well-founded. In such a context the above reasoning falls apart as we cannot reason externally to the model to construct iterated truth predicates. (See this previous blog post of mine for a taste of the pitfalls in considering iterated truth predicates when nonstandardness rears its head.)

However, this issue is avoided so long as we don’t try to fly too high. It was safe to reason about \mathsf{ETR}_\mathrm{Ord} because \mathrm{Ord} \times \omega, ordered lexicographically, is well-founded in any model of \mathsf{GBC}. In general, if \mathtt{t} is a term for a class well-order which is well-founded in any model of \mathsf{GBC} then \mathtt{t} \cdot \omega will always be well-founded and so it is meaningful to talk about the least \eta so that the \mathtt{t} \cdot n-iterated truth predicate is strongly amenable over L_\eta (for all n < \omega). This yields minimal models of stronger fragments than \mathsf{ETR}_\mathrm{Ord}—for example, \mathsf{ETR}_{\mathrm{Ord}^2} or \mathsf{ETR}_{\mathrm{Ord}^\mathrm{Ord}}—but how high does this get us? Can we get as high as all the first-order definable class well-orders?

Question. If \mathsf{GBC} proves that the class defined by \varphi(x,y) doesn’t contain an infinite descending sequence, where \varphi is a first-order formula with no class parameters, then must it be that (M,\mathcal X) \models \mathsf{GBC} being transitive implies \varphi[M] truly is well-founded? Asked in the negative, is it possible to have a transitive model of \mathsf{GBC} which wrongly believes that the class defined by \varphi is well-founded?

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.

Non-hyperfinite countable equivalence relations

This will be a talk at the CUNY Models of Peano Arithmetic seminar on Wednesday, March 15th 2017. (Added later: the talk overspilled into the next two weeks of the MoPA seminar.)

I will present an argument of the Slaman–Steel theorem that the equivalence relation E_\infty is not hyperfinite. Time permitting, I will explain a potential connection between this argument and the classification problem for models of arithmetic.