Recursively saturated and rather classless

A mathematics blog by Kameryn Williams

Category: MoST

Minimal models for second-order set theories

This is a contributed talk at the 2018 ASL North American Annual Meeting on 17 May 2018.

Shepherdson and, independently, Cohen showed that there is a least transitive model of \mathsf{ZFC}, i.e. a transitive model of \mathsf{ZFC} which is contained inside every transitive model of \mathsf{ZFC}. An analogous question can be asked of other set theories. I will consider second-order set theories, those which have both sets and classes as their objects. It was known to Shepherdson that von Neumann–Bernays–Gödel set theory \mathsf{NBG} has a smallest transitive model. I will show that this phenomenon fails for stronger second-order set theories: there is no least transitive model of Kelley–Morse set theory \mathsf{KM}. Indeed, there is no least transitive model of \mathsf{NBG} + \Pi^1_1-Comprehension, nor any computably enumerable extension thereof. On the other hand, fragments of \mathsf{NBG} + Elementary Transfinite Recursion, which sit between \mathsf{NBG} and \Pi^1_1-Comprehension in consistency strength, do have least transitive models.


Every countable model of set theory end-extends to a model of V = L

This theorem has popped up in my life a few times in the past week, and it’s one of the coolest results I know of, so I wanted to share it with the world.

Theorem (Barwise): Every countable transitive model of \mathsf{ZF} has an end-extension to a model of \mathsf{ZFC} + V = L.

If M and N are models of set theory then N is an end-extension of M if for every a \in M and every b \in N if N \models b \in a then b \in M. That is, any new elements in N cannot appear as members of old elements, and must come at the end of the epsilon relation. It’s easy to see that if N is an elementary end extension of M then in fact N is a rank-extension of M—every new element has rank above the ordinals of M. But if we don’t have elementarity then an end-extension can be quite far from a rank-extension. For instance, if M is an inner model of N then N end-extends M.

If you’re like me when I first learned of this result, your reaction at this point is probably disbelief. So let’s see why Barwise’s theorem is true. We will use the following version of Shoenfield’s lemma.

Lemma (Shoenfield): Work over \mathsf{ZF} and let \varphi be a \Sigma_1 formula without parameters. Then \varphi implies \varphi^L.

Let me give a proof that assumes a fragment of choice. Chapter V.8 of Barwise’s Admissible Sets and Structures has a proof that goes through without using any choice. (Thanks to Asaf Karagila for catching my mistake here.)

Proof: The usual version of Shoenfield’s lemma is that (lightface) \Sigma^1_2 formulae, i.e. formulae of the form “there is a real so that for all reals some arithmetical property (without parameters) holds”, are absolute between V and L. Let’s see how to get this other form.

Suppose that \varphi = \exists x \psi(x) is true, where \psi(x) only has bounded quantifiers. Then if A is any transitive set containing a witness for \psi(x) we have A \models \varphi. There must be such A, so by downward Löwenheim–Skolem we get a countable transitive A so that A \models \varphi. But the assertion that there is countable such A is \Sigma^1_2—there is a real coding a well-founded structure so that blah blah. So it must also be true in L that there is such an A. And \Sigma_1 things are upward absolute between transitive models, so L \models \varphi, as desired.

We can now prove Barwise’s theorem.

Proof of Barwise’s theorem: Let M \models \mathsf{ZF} be countable and transitive. We will consider a theory  in the logic \mathcal L_M, the countable admissible fragment of \mathcal L_{\infty,\omega} associated with M (that is, \mathcal L_M = (\mathcal L_{\infty,\omega})^M). Namely, our theory T has as axioms:

  • Each axiom of \mathsf{ZF} and
  • The infinitary \in-diagram of M, i.e. all sentences of the form x \in a \Leftrightarrow \bigvee_{b \in a} x = b, where “x = b” is an abbreviation for the \mathcal L_M-formula defining b. (Think of how every hereditarily finite set is definable in \mathcal L_{\omega,\omega}.)

Then T is definable over M by a \Sigma_1 formula \tau(x). The point of including the infinitary \in-diagram of M in T is that it ensures that any model of T must end-extend M.

Now suppose towards a contradiction that there is no model of T + V = L. Thus, T \models V \ne L. So by the Barwise completeness theorem we get that T \vdash V \ne L is true in M. (This is where we use the assumption that M is countable.) Similar to how ordinary proofs in first-order logic can only use finitely many axioms, infinitary proofs can only use set-many axioms. So M thinks that there is a proof of V \ne L from the axioms of T which only uses set-many axioms. A bit more formally, M satisfies that there is a set \Phi so that every x \in \Phi has \tau(x) and there is an infinitary proof of \bigwedge \Phi \Rightarrow V \ne L. Stare at that for a moment and convince yourself that this is a \Sigma_1 assertion (because it is \Sigma_1 to say that there is an infinitary proof of such and such).

By Shoenfield, we get that L^M satisfies the same thing. And in L^M we have that \tau(x) defines the \mathcal L_{L^M}-theory whose axioms are \mathsf{ZF} and the infinitary \in-diagram of L^M. Call this theory T'. So we get that there is T_0 \subseteq T' with T_0 \in L^M so that T_0 \models V \ne L. But this is impossible, since L^M \models T_0 + V=L. So our original assumption that T + V = L has no model must be false, so M has an end-extension to a model of \mathsf{ZFC} + V=L.

Let me put a horizontal rule here to indicate that you should pause for a moment to appreciate the beauty of Barwise’s proof.

Why isn’t this theorem paradoxical? Suppose we started with, say, a countable transitive model of \mathsf{ZFC} + 0^\sharp exists, where this model has the real 0^\sharp. How could we possibly end-extend to a model of V = L? Wouldn’t that contradict the well-known fact that 0^\sharp is not in L?

The answer is that the end-extension Barwise gives us must, in this case, be nonstandard. Our end-extension sees the real 0^\sharp and thinks that it is constructible, but it only shows up in L_\alpha for some ersatz, ill-founded ‘ordinal’ \alpha. As a consequence, the end-extension does not recognize that the set we externally can see is 0^\sharp really is 0^\sharp. It thinks it’s just some constructible real. Similarly, we could start with a model which has measurable cardinals, or supercompact cardinals, or any other creature of the higher infinite, and the end-extension will think that all the witnessing measures are constructible (but appearing at some nonstandard stage in the construction of L).

So what Barwise gives us is another example of the nonabsoluteness phenomenon for nonstandard models. The classical example of this is provability, where end-extending a model of arithmetic can change what is provable. The standard model thinks that there is no proof of 0=1 from the axioms of Peano arithmetic, but if we end extend to the right nonstandard model we can get such a ‘proof’. Or phrased in terms of Turing machines: the TM which searches for a proof of 0=1 from the axioms of PA doesn’t halt. But it can halt if we wait a nonstandard amount of time (in the right model). And in light of Koepke’s work on the connection between infinite time&space Turing machines and constructibility, the Barwise phenomenon can also be phrased in terms of computability: While 0^\sharp is not computable (from finitely many ordinal parameters) by a Turing machine with <\mathrm{Ord} time and space, it does become ‘computable’ if we allow a nonstandard amount of time and space (in the right model).

Finally, let me remark that Barwise’s theorem also holds for countable ill-founded models. But the proof requires going through the admissible cover. This is a rather fantastic piece of machinery (also due to Barwise), but expositing it would be too much for this blog post. See the appendix to Barwise’s Admissible Sets and Structures for facts about the admissible cover, as well as a proof for the ill-founded version of his theorem.


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.



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

Killing truth

It is not difficult to construct models of \mathsf{ZFC} whose truth predicate is not strongly amenable, where X \subseteq M is strongly amenable if the structure (M,X) satisfies the Collection and Separation schemata in the expanded language. Namely, this can be accomplished by considering a pointwise definable model of \mathsf{ZFC}, such as the Shepherdson–Cohen least transitive model. The truth predicate for the model M reveals that it is countable, allowing one to define a surjection \omega^M \to M. This witnesses a failure of Replacement (in the expanded language).

On the other hand, one can find models whose truth predicate is strongly amenable. If (M,\mathcal X) \models \mathsf{GBC} contains the truth predicate for M then its truth predicate must be strongly amenable, due to the Class Replacement and Class Comprehension axioms of \mathsf{GBC}. In particular, if (M,\mathcal X) satisfies Kelley–Morse set theory (or any other second-order set theory which proves the existence of the truth predicate) then truth will be strongly amenable for M.

Let’s consider those models whose truth is strongly amenable. If we have a \mathsf{GBC}-realization for such a model can we always add more classes  (but not sets!) to expand it to a \mathsf{GBC} model which contains the truth predicate?

The answer is no. For countable models we can kill truth with the right \mathsf{GBC}-realization, so that no matter what new classes we add we cannot have the truth predicate without violating Class Replacement.

Proposition: Let M \models \mathsf{ZFC} be a countable \omega-model. Then there is a \mathsf{GBC}-realization \mathcal X \subseteq \mathcal P(M)  for M so that no \mathsf{GBC}-realization \mathcal Y \supseteq \mathcal X can contain the truth predicate for M.

The purpose of requiring M to have a well-founded \omega is the Krajewski phenomenon that countable \omega-nonstandard models of set theory which admit ‘truth predicates’ which measure the truth of all—internal, possibly nonstandard—formulae (full satisfaction classes, to use the jargon) admit continuum many different ones. So in such case there is not a unique object to kill off (indeed, it’s not sensible to speak of the truth predicate for M in the absence of an already-fixed second-order part) and the situation becomes much trickier.

But more on that later. Let’s see why this proposition is true.

Proof: Suppose that truth is strongly amenable for M. Otherwise, no \mathsf{GBC}-realization for M can contain the truth predicate and there is nothing to prove. We will produce the desired \mathcal X by adding a carefully constructed Cohen-generic subclass of \mathrm{Ord}. Let \mathbb C be this class forcing, i.e. the partially ordered class consisting of set-sized partial functions \mathrm{Ord} \to 2, ordered by reverse inclusion. This forcing is \kappa-closed and \kappa-distributive for every cardinal \kappa so it does not add new sets.

Claim: There is a sequence \langle D_i : i \in \mathrm{Ord} \rangle of definable dense subclasses of \mathbb C which is (1) definable from the truth predicate for M and (2) meeting every D_i is sufficient to guarantee a filter is generic over M.

It is clear that the collection of dense subclasses of \mathbb C is definable from the truth predicate; the truth predicate allows one to see whether \varphi(x,a) defines a dense subclass of \mathbb C and so the whole collection can be indexed by (\varphi, a). The trick is to extract a sequence of ordertype \mathrm{Ord}. This is trivial if M has a definable global well-order, but in general this may not be true. In such case, use that \mathbb C is \kappa-distributive for every \kappa. So given a set-sized collection of dense subclasses we can find a single dense subclass below all of them. So we get the D_is as in the claim by taking D_i to be below all dense subclasses definable from parameters in V_i.

We will now use this \langle D_i : i \in \mathrm{Ord} \rangle to define a Cohen-generic subclass C of \mathrm{Ord}. Externally to the model, fix an \omega-sequence cofinal in \mathrm{Ord}^M. Think of this sequence as an \mathrm{Ord}^M-length binary sequence \langle b_i : i \in \mathrm{Ord} \rangle, consisting mostly of zeros with the rare one. This sequence is amenable over M, since its initial segments have only finitely many ones. On the other hand, it is not strongly amenable since from this sequence can be defined a cofinal map \omega \to \mathrm{Ord}, contradicting an instance of Replacement.

We build C in \mathrm{Ord}^M steps. Start with c_0 = \emptyset. Given c_i let c_{i+1}' = c_i {}^\smallfrown \langle b_i \rangle and then extend c_{i+1}' to c_{i+1} meeting D_i, where we require the extension to be minimal in length to meet D_i. (If there is more than one way to meet D_i of minimal length, choose between them arbitrarily.) At limit stages take unions of the previous stages. Finally, set C = \bigcup_{i \in \mathrm{Ord}} c_i. Then C is generic over M since it meets every D_i. But hidden within C is this bad sequence \langle b_i \rangle.

I claim now that from both C and the truth predicate for M one can define \langle b_i \rangle. This is done inductively. We know b_0 because it is the first bit of C. From the truth predicate we know the minimal amount we have to extend \langle b_0 \rangle in order to meet D_0, because the sequence \langle D_i \rangle is definable from the truth predicate. So we can recover c_1. We now repeat this process, discovering b_2 as the first bit of C after c_1 and thereby can define c_2 by knowing the minimal length we had to extend to meet D_2. And so on we define b_i and c_i for all i \in \mathrm{Ord}^M. So if we have access to both C and the truth predicate then we can define the sequence \langle b_i \rangle.

But if we can define the bad sequence then our model must fail to satisfy Class Replacement. Thus, there can be no \mathsf{GBC}-realization for $M$ which contains both C and the truth predicate for M. So \mathrm{Def}(M;C) is a \mathsf{GBC}-realization for M which cannot be extended to a \mathsf{GBC}-realization which contains the truth predicate, as desired. (To see (M,\mathrm{Def}(M;C)) \models \mathsf{GBC} observe that every Cohen-generic subclass of \mathrm{Ord} codes a global well-order by comparing where each set is first coded into the generic.) ∎

As mentioned above, Kelley–Morse proves the existence of the truth predicate for the first-order part, as do many much weaker theories. As a consequence we get \mathsf{GBC} models which cannot be expanded by adding classes to get a model of \mathsf{KM}, even if the first-order part has some other \mathsf{KM}-realization.

Corollary: Let M \models \mathsf{ZFC} be any countable \omega-model. Then M has a \mathsf{GBC}-realization which cannot be extended to a \mathsf{KM}-realization. The same is true if \mathsf{KM} is replaced by \mathsf{GBC} plus Elementary Transfinite Recursion, or even \mathsf{GBC} + \mathsf{ETR}_\omega.

What this result suggest is that it matters how one builds up one’s classes. It is not difficult to see that, say, \mathsf{KM} proves there exist classes of ordinals which are Cohen-generic over the definable classes. (The truth predicate lets us list the definable dense subclasses of the forcing, so they can be met one at a time.) So if we want to build up a model of \mathsf{KM} from a fixed universe of sets we must add Cohen-generics at some point. The above shows that it matters which generics we pick. One wrong step along the way and we stumble off the narrow path leading to paradise.

Observe that the proposition relativizes. Fixing a possible class X \subseteq M if X can be put in any \mathsf{GBC}-realization for M then there is a \mathsf{GBC}-realization for M containing X which cannot be extended to one containing the truth predicate relative to the parameter X. As a consequence, one can find \mathsf{GBC}-realizations for any strong enough countable \omega-model M which contain an iterated truth predicate of length \Gamma but which cannot be extended to a \mathsf{GBC}-realization containing an iterated truth prediacte of length \Gamma + 1.

As a coda, let me return \omega-nonstandard models. Here, things go badly. As mentioned earlier, Krajewski showed that if a countable \omega-nonstandard model of set theory admits a ‘truth predicate’ (full satisfaction class) then it admits continuum many different ones. So killing off one possible truth predicate will not immediately ensure that the classes cannot be expanded to include truth; perhaps some other full satisfaction class can be added to the classes to be truth. But a version of the above argument does show that we can kill off individual full satisfaction classes. (A strongly amenable full satisfaction class will tell us about dense subclasses of the Cohen-forcing which are ‘defined’ using a nonstandard formula, but it will also tell us about all the really definable dense subclasses, so it is good enough.) Can we kill off all the full satisfaction classes? I don’t (yet?) know!

Question: If M \models \mathsf{ZFC} is countable and \omega-nonstandard must it be the case that there is a \mathsf{GBC}-realization \mathcal X for M so that no matter how we expand \mathcal X we never get \mathcal Y so that (M,\mathcal Y) satisfies \mathsf{GBC} plus “there is a truth predicate for first-order truth”?


Strong second-order set theories do not have least transitive models

This will be a talk at the University of Pennsylvania Logic and Computation Seminar on Monday, November 13. See also their page for the talk. Slides available here.

Shepherdson and Cohen independently showed that (if there is any transitive model of \mathsf{ZFC}) there is a least transitive model of \mathsf{ZFC}. That is, there is a transitive set M so that (M,\in) \models \mathsf{ZFC} and if N is any transitive model of \mathsf{ZFC} then M \subseteq N. We can ask the same question for theories extending \mathsf{ZFC}. For some fixed set theory T, does T have a least transitive model?

I will look at this question where T is a second-order set theory.  Two major second-order set theories of interest are Gödel–Bernays set theory \mathsf{GBC} and Kelley–Morse set theory \mathsf{KM}. The weaker of the two is \mathsf{GBC}, which is conservative over \mathsf{ZFC} while \mathsf{KM} is much stronger.

As an immediate corollary of the Shepherdson–Cohen result we get that there is a least transitive model of \mathsf{GBC}. The case for \mathsf{KM} is more difficult and indeed, has a negative answer. I will show that there is no least transitive model of \mathsf{KM}. Along the way we will build Gödel’s constructible universe above sets and into the proper classes, unroll models of second-order set theory into first-order models, and dip our toes into Barwise theory and the admissible cover. Time permitting I will mention some results and open questions about \mathsf{GBC} + Elementary Transfinite Recursion, which is intermediate between \mathsf{GBC} and \mathsf{KM} in strength.


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.


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.


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

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?