= Solution
For the <Ehrenfeucht-Mostowski theorem>, let $M$ be an infinite <first-order structure> and $I$ any linear order. Choose a full <Skolem expansion> $M^*$: add witness functions for existential formulas, repeat in the expanded languages, and take their union. We will construct a model of its theory containing distinct generators $c_i$, $i\in I$, forming an <order-indiscernible sequence>.
Adjoin the elementary diagram of $M^*$, the inequalities $c_i\ne c_j$ for $i\ne j$, and for every expanded-language formula $\phi(x_1,\ldots,x_r)$ and every two increasing $r$-tuples of indices, the sentences
$$
\phi(c_{i_1},\ldots,c_{i_r})\leftrightarrow\phi(c_{j_1},\ldots,c_{j_r}).
$$
Every finite subcollection is satisfiable in $M^*$. To prove this, choose a countably infinite sequence of distinct elements of $M$, and for each of the finitely many relevant arities color its increasing index tuples by the finite vector of truth values of the formulas of that arity. Repeated applications of the <Ramsey's theorem> give an infinite subsequence homogeneous for all these finitely many <finite colorings>. Interpret the finitely many mentioned $c_i$ by its elements in their index order. All indiscernibility and distinctness constraints hold, and the finite diagram fragment holds because the ambient structure is still $M^*$.
By <compactness theorem>, a model $N^*$ of the full enlarged theory exists. Its <Skolem hull> $H$ generated by the $c_i$ is elementary: whenever an existential formula with parameters in $H$ holds in $N^*$, its chosen witness function returns a value in $H$, so the <Tarski-Vaught test> applies. Its reduct is a model of $\operatorname{Th}(M)$. If the index order has size $\kappa$, the hull has size at most $\kappa+|L|+\aleph_0$, and it contains $|I|$ distinct generators.
Every order automorphism $h$ of $I$ induces the automorphism
$$
t(c_{i_1},\ldots,c_{i_r})\longmapsto t(c_{h(i_1)},\ldots,c_{h(i_r)}).
$$
To check well-definedness, write any two terms being compared over the same increasing list of their generators. Their equality is an expanded-language formula; indiscernibility of the <order-indiscernible sequence> preserves its truth under $h$. The same argument preserves each relation, and the term construction preserves the functions. Applying $h^{-1}$ gives the inverse. The extension is unique in the specified Skolem language since every hull element is a term in the generators; no uniqueness among all automorphisms of the reduct is being asserted. This proves the <Ehrenfeucht-Mostowski theorem>, including its usual automorphism consequence.
For <simple typed set theory with atoms>, use sorts $0,1,\ldots$, predicates $S_i$ for sets, and typed membership from sort $i$ to sort $i+1$. Atoms have no members, extensionality compares sets, and every well-typed formula defines a set of the next sort. <Typical ambiguity> is the schema $\phi\leftrightarrow\phi^+$ for every closed typed sentence, where the superscript raises all types by one.
Here are concrete full typed models before imposing the ambiguity schema. Choose increasing natural numbers $n_{-1}<n_0<n_1<\cdots$ and set
$$
D_i=V_{\omega+2n_i},\qquad S_i=\mathcal P(D_{i-1})\subseteq D_i.
$$
The auxiliary $D_{-1}$ merely interprets the set predicate at the lowest sort. Define typed membership by
$$
x\mathrel{\in_i}y\quad\Longleftrightarrow\quad y\in S_{i+1}\text{ and }x\in y.
$$
Then the other objects of $D_{i+1}$ are atoms, regardless of their old membership. Every subset of $D_i$ has its representative in $S_{i+1}$, giving comprehension even for formulas with higher-sort quantifiers and parameters. Extensionality holds for the set representatives and atoms have no typed members. The rank gaps leave infinitely many atoms at each sort, and all sorts are infinite.
Consider finitely many ambiguity instances with unraised sentences $\phi_1,\ldots,\phi_t$, and choose a fixed window length $r$ sufficient to include every sort used and its auxiliary predecessor. Color every increasing $r$-tuple of natural numbers by the vector of truth values of these unraised sentences in its finite rank-window interpretation. There are only $2^t$ colors. The <Ramsey's theorem> gives an infinite homogeneous set. Choose $r+1$ successive points from it. The first $r$ points and last $r$ points have the same color, while the latter interpretation of $\phi_j$ is exactly the former model's interpretation of $\phi_j^+$. The auxiliary predecessor shifts too, so this remains true for sentences mentioning the lowest set predicate. Extend the chosen rank sequence arbitrarily to interpret the remaining sorts. This yields a model of typed set theory satisfying all the specified ambiguity instances.
Thus every finite subset of the typed axioms together with all ambiguity instances has a model. Applying multisorted <compactness theorem> gives
$$
\boxed{\operatorname{Con}(\mathrm{TSTU}+\mathrm{Typical\ ambiguity}).}
$$
The final model satisfies first-order typed comprehension, with quantification over its own sorts and sets as in <Henkin semantics>.
Back to article page
