= Solution
A useful precise form of the <Ehrenfeucht-Mostowski theorem> is this: for an infinite structure $M$ and any linear order $I$, a model of $\operatorname{Th}(M)$ can be generated as a <Skolem hull> by distinct order indiscernibles $(a_i)_{i\in I}$. Every <order automorphism> of $I$ extends to an automorphism of that hull in the chosen Skolem language. One may first name all elements of $M$, giving an <elementary extension> containing the original structure. The generation and uniqueness assertions concern this specified expansion, not arbitrary automorphisms of its reduct.
Choose a <Skolem expansion> $M^*$: for each existential formula add a function selecting a witness whenever one exists. Introduce constants $c_i$ for $i\in I$. Take the theory of $M^*$, distinctness of these constants, and all equivalences
$$
\varphi(c_{i_1},\ldots,c_{i_r})\leftrightarrow\varphi(c_{j_1},\ldots,c_{j_r})
\quad(i_1<\cdots<i_r,\ j_1<\cdots<j_r).
$$
The formulas here are in the fixed expanded language, without the newly added $c_i$ as extra parameters. If naming $M$, use its complete elementary diagram and allow those original names in the formulas.
Every finite fragment has a model by <Ramsey's theorem>. Only finitely many formulas and constants occur. Take a sequence of distinct elements of $M$. For each arity appearing, color the increasing tuples from this sequence by the finite vector of truth values of all formulas of that arity. Successive Ramsey thinning gives an infinite subset homogeneous for each of these finitely many colorings. Assign the finitely many constants in increasing order to distinct elements of this subset. This satisfies every displayed equivalence in the fragment; the original theory is satisfied because the underlying structure remains $M^*$. <Compactness> now gives a model of the full theory, with the required <order-indiscernible sequence>.
The substructure generated by the constants under the <Skolem functions> is elementary: any existential formula with parameters which are terms in the generators has its Skolem witness in that same hull. If $g$ is an <order automorphism> of $I$, define
$$
t(a_{i_1},\ldots,a_{i_r})\longmapsto t(a_{g(i_1)},\ldots,a_{g(i_r)}).
$$
Indiscernibility makes this well-defined, by applying it to the equation between any two term representations using the increasing tuple of all their indices. The same argument preserves every relation and function; $g^{-1}$ supplies the inverse. It is unique in the generated Skolem structure. This completes the Ramsey proof, rather than stopping at the existence of indiscernibles.
For <simple typed set theory with atoms>, use sorts $D_0,D_1,\ldots$ and membership only from $D_i$ to $D_{i+1}$. A set predicate distinguishes sets from atoms, <extensionality> compares sets of the same positive type, and comprehension produces in type $i+1$ every subset of $D_i$ defined by a well-typed formula. Atoms have no members. First-order models use <Henkin semantics>; they are not required to have their next domain equal to the full external <power set>. <Typical ambiguity> is the schema $\phi\leftrightarrow\phi^+$ for each closed sentence, where every sort index in $\phi^+$ is raised by one.
We show finite satisfiability of this entire typed theory with ambiguity. Choose a list of ranks $\rho_0<\rho_1<\cdots$ above $\omega$, spaced by at least two. For a finite increasing selection of ranks $r_{-1}<r_0<\cdots<r_m$, let
$$
D_i=V_{r_i},\qquad S_i=\mathcal P(V_{r_{i-1}}),
$$
where $S_i$ is the set of objects declared to be sets at type $i$. Membership from $D_i$ to $D_{i+1}$ is ordinary membership restricted to objects of $S_{i+1}=\mathcal P(D_i)$; all other type-$i+1$ objects are atoms. The spacing puts $\mathcal P(D_i)$ inside $D_{i+1}$. Thus comprehension and set <extensionality> hold exactly, and atoms have no typed members. There are infinitely many objects at every visible type, so any usual typed infinity requirement also holds.
The auxiliary rank $r_{-1}$ provides a uniform interpretation if a set predicate is allowed at type zero; no type-minus-one domain is used in the theory. This avoids artificially declaring all type-zero objects to be atoms, which would not be invariant under type-raising. If the language has no type-zero set predicate, simply ignore this auxiliary interpretation.
A finite set of ambiguity instances uses finitely many closed sentences of bounded highest type, say at most $m$. Color increasing $(m+2)$-tuples of ranks by their finite truth vector in the structure with visible domains $D_0,\ldots,D_m$ and the auxiliary preceding rank. <Ramsey's theorem> gives an infinite homogeneous rank set. Choose $m+3$ consecutive ranks from it and build the hierarchy on all these ranks. The first window evaluates each original sentence; shifting the window one place evaluates its uniform type-raise. Homogeneity makes the truth vectors equal. All finite typed axioms and the selected ambiguity instances therefore hold together. Choosing $m$ large enough covers every sort needed by the finite fragment. Many-sorted <compactness>, equivalently ordinary first-order <compactness> after encoding sorts, yields
$$
\boxed{\operatorname{Con}(\mathrm{TSTU}+\text{typical ambiguity}).}
$$
This is a model existence argument in the ambient set theory; no equality of adjacent type cardinalities is claimed. The gaps between ranks supply atoms, and the ambiguity is about truth of sentences, not a bijection between domains.
Back to article page
