### 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?