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 . Of course, we can ask a similar question about other set theories: given a set theory , is there is a smallest transitive model of ? This question makes sense even when is a second-order theory, such as or . A second-order model is transitive when its set-set and set-class elementhood relations are the true .
Theorem (Shepardson). There is a least transitive model of .
Namely, the least transitive model of is , where is the least transitive model of .
However, if we ask the same question for second-order set theories much stronger than we get a negative answer.
Theorem (W., not yet published). There is no transitive model of which is contained in all transitive models of .
What happens if we weaken ? If we weaken it all the way down to , then we get the phenomenon of minimal models. If we only weaken it a little bit, say to for , then we still do not have least transitive models.
What if we weaken it a lot, but not all the way down to ? Or, starting from the other direction, how much can we strengthen and retain the existence of minimal models?
Of course, this question must be made more precise. We can come up with silly strengthenings of which do not have least transitive models. Consider the theory consisting of 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 and have minimal models?
One natural theory is , a strengthening of which also asserts that any transfinite recursion of a first-order property along a well-founded class relation has a solution. ( stands for “elementary transfinite recursion”, à la the arithmetical transfinite recursion axiom from arithmetic.) This theory sits between and in strength. It’s stronger than as it proves, for instance, the existence of a truth predicate for first-order formulae. It’s weaker than as it is provable from .
Is there a least transitive model of ? While I do not have an answer for this, I do have an answer for some fragments of .
We can weaker by only requiring that we have solutions for recursions along relations of low rank. If is an ordinal then asserts that we have solutions for recursions of rank . Similarly, asserts that we have solutions for recursions of rank .
Proposition. If or so that , then there is a least transitive model of .
In the remainder of this post I want to prove this proposition.
The first step is to reduce to having solutions just for certain recursions. Gitman and Hamkins showed that is equivalent to having, for any class well-order and any class , an iterated truth predicate along relative to the class . (See their Theorem 8.) Staring at their proof for a few moments, one sees that they showed that whenever that is equivalent to having iterated truth predicates along relative to any class .
Thus, we can build models of just by ensuring that we have enough iterated truth predicates.
Lemma. Suppose that is transitive and has a global well-order which is first-order definable without any class parameters, where or . Then has a smallest -realization. That is, there is so that and whenever we have .
Proof: Let . Then, , because has a definable global well-order. However, as it doesn’t even have a truth predicate. Let be the -iterated truth predicate for relative to . Then, because , if we set we have . We still do not have a model of , because doesn’t contain the -iterated truth predicate relative to . So let be this truth predicate and set .
Keep going on in this manner. Having defined and , next let be the -iterated truth predicate relative to and set .
After steps, set . We get that because it is the union of an increasing chain of models of . More, for any class we have for some . Hence, will contain the -iterated truth predicate for relative to . Altogether, this gives that .
It remains only to see that is contained in every -realization for . But this is simply because any must contain for every . Since is the smallest -realization for containing all of the , it must be contained within . ∎
Note that we could have built in a single step as , i.e. the smallest -realization for which contains the -iterated truth predicate for for all .
This argument needs that truth predicates for are unique, which is true for transitive . On the other hand, -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 be the least ordinal so that is -realizable. By the above lemma, has a least -realization . I claim that is the least transitive model of .
To see this, take transitive . There are two cases to consider. The first is if . We need to see that for each . This can be seen by noticing that and using that whenever . The second case is if . In this case, , so for and thus . ∎
What if we want to go beyond ? 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, or 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 because , ordered lexicographically, is well-founded in any model of . In general, if is a term for a class well-order which is well-founded in any model of then will always be well-founded and so it is meaningful to talk about the least so that the -iterated truth predicate is strongly amenable over (for all ). This yields minimal models of stronger fragments than —for example, or —but how high does this get us? Can we get as high as all the first-order definable class well-orders?
Question. If proves that the class defined by doesn’t contain an infinite descending sequence, where is a first-order formula with no class parameters, then must it be that being transitive implies truly is well-founded? Asked in the negative, is it possible to have a transitive model of which wrongly believes that the class defined by is well-founded?