We define a new theory to be, approximately, a “binary tree” of equivalence relations, of depth . That is, each equivalence class at level splits into exactly two classes at level , assuming that’s well-defined.
More precisely, for any ordinal , we define the language , where each is a binary relation. The theory states that each is an equivalence relation, and if , then every splits into precisely two classes. More axiomatically, for any in the structure, there is a in the structure where and , but for any in the structure, if , then either or .
The tree motivation yields an “intended model,” (which is not necessarily a prime model) denoted , where the underlying set is the space of functions from to , and the equivalence relation is agreement on the subset . It is clear that this is an equivalence relation, and that each -class (represented by a “partial function” from to ) indeed refines into exactly two -classes (extensions of that partial function, which send $\beta$ itself to either $0$ or $1$).
If is a nonzero limit ordinal, then every equivalence class, at every height, is subdivided at the next height, so must have at least 2 elements. But it’s then subdivided again, and so on, so in fact, every equivalence class at every level must be infinite. This is not actually true if is a successor ordinal, so for this (and a few other) reasons, we will always assume is a nonzero limit ordinal. In fact the next theorem is not true if is a successor ordinal!
has quantifier elimination.
Suppose that , that is a tuple from the intersection, and that is an open formula with free. Suppose also that for some , we have . It is then sufficient to show that .
So let be the largest ordinal (less than ) where appears positively in , for some . If there are none, we just let , where is just always true. We will now produce a solution to in .
We may assume (by using the disjunctive normal form, then passing to a positive disjunct) that is a conjunction of atoms, some positive and some negative. Let be the highest ordinal such that some appears in $\phi$, and start with the -class of in . We will go term-by-term in and generate an infinite number of solutions.
First, all positive terms are already satisfied, since they must be of the form , and since models , we must have all -equivalent, since by construction, and the equivalence relations refine their predecessors.
So for negative terms, note that if and appears, then it’s already satisfied, since as before, and are -equivalent. So if , then , so if , then .
So we now pass to the case where , and are concerned with the case where appears in , but actually holds. But since , there are multiple -classes within our working set, and clearly only one class can violate our constraint. Thus we can simply pass to any of the other -classes and stay in infinite set of solutions.
Constructively, we work within the set of solutions to our largest positive constraint. Then, in ascending order in , we move to -classes which satisfy our negative constraints. This terminates in finite time (since formulas are finite) and we have our solution in . This completes the proof.
has a prime model.
The “intended model,” , is quite obviously larger than the language at hand, but a slight modification of our construction will yield a substructure of we will call . In fact the substructure will just be those functions which are zero on a cofinite subset of . This is still a model of , by the same proof as before- we just don’t have so many classes actually represented. Note that in this model (and in the intended model, though not all models), if is a limit ordinal, then . That is, if two functions disagree at a limit stage, then they disagree on a previous stage.
Claim: The lexicographic ordering on is a well-order.
In all cases, if in , then there is a such that and agree up to , but then . Then , then the relevant point of last agreement must have . Thus, any infinite downward chain in yields an infinite downward chain of ordinals, which is impossible.
Now, from the claim, we can use strong induction to build an injection from into any arbitrary model . Pick the target of the first element (the zero function) arbitrarily. For any other function , pick the last where , and let be the function which agrees everywhere with except at , and where . Then , so already has an image in – call it .
We want an which is -equivalent with if and only if . But the -class is infinite and refines into two -classes, so choose arbitrarily from the class which doesn't contain .
This gives an injection which preserves every and its negation. By quantifier elimination, this is then an elementary map, yielding primality. Completeness follows immediately- if and only if , so , and is complete.
We use the local form of stability. By quantifier elimination, it is sufficient to show that open formulas are stable. The class of stable formulas is also closed under negation and conjunction, so it sufficient to show that positive atoms are stable.
Now we show that for any atom and any set , every type in is definable. But this is pretty clear: any atom is either of the form or . In either case, if the atom never appears positively, then it admits a definition of . If it does appear positively, say as or , then it can be defined by or respectively, since both equality and are equivalence relations.
Superstability is equivalent to the property that there is no infinite forking chain. By quantifier elimination and the usual reductions, this would be an element and a sequence such that, if , then forks with over for every .
Claim: forks with over if and only if, for some and some , we have , but for every and every , we have .
This shows that an infinite forking chain of types yields an infinite decreasing chain of ordinals, which is impossible. So must be superstable.