= Solution
For the <Ehrenfeucht-Mostowski theorem>, start with an infinite structure $M$ and a <total order> $I$. Choose a <Skolem expansion> $M^*$, and adjoin constants $c_i$ for $i\in I$. Require the <elementary diagram> of $M^*$, distinctness of these new constants, and the <order-indiscernible sequence> schema: any two increasing tuples of the $c_i$ of the same length satisfy the same <first-order formulas> in the expanded language. Every finite fragment mentions finitely many new constants and finitely many <first-order formulas>. Enumerate a countably infinite subset of $M$. For each of the finitely many <first-order formulas>, color its increasing tuples by its truth value in $M^*$, including whatever fixed parameters occur in the fragment. Successive applications of the infinite <Ramsey theorem> leave an infinite <subset> homogeneous for all these colorings. Assign the finitely many new constants to distinct elements of this <subset> in their index order. Their finite indiscernibility requirements and the <elementary diagram> are then simultaneously satisfied.
The <compactness theorem> supplies an <elementary extension> $N^*$ containing the required distinct indiscernibles. Their <Skolem hull> is an <elementary substructure>: an existential <first-order formula> true of its elements has its chosen Skolem-function witness in the hull, so the <Tarski-Vaught test> applies. Any <order automorphism> $\sigma$ of $I$ acts on this hull by
$$
t(c_{i_1},\ldots,c_{i_n})\longmapsto t(c_{\sigma(i_1)},\ldots,c_{\sigma(i_n)}).
$$
Indiscernibility makes this well defined, since every equality of two term representations is preserved. The same argument preserves every <first-order formula>; the inverse is given by $\sigma^{-1}$. Thus it is an automorphism, uniquely determined in the language of the chosen <Skolem expansion> by its values on the generators. This proves both the indiscernible-model and automorphism forms of the <Ehrenfeucht-Mostowski theorem>. Uniqueness is not claimed for automorphisms of the reduct which need not preserve the chosen <Skolem functions>.
For <simple typed set theory with atoms>, write $S_i$ for the <set> predicate at sort $i$. Members have sort one lower; <urelements> have no typed members, <extensionality> applies to <sets>, and every well-typed <first-order formula> defines a <set> at the next sort. <Typical ambiguity> adds $\phi\leftrightarrow\phi^+$ for each closed sentence, where $+$ raises every sort by one. We prove finite satisfiability using <Ramsey theorem>, rather than assuming that adjacent sorts have the same <cardinality>.
Let $X_n=V_{\omega+2n}$. If $n<m$, then $\mathcal P(X_n)\subseteq X_m$. For increasing integers $h_0<h_1<h_2<\cdots$, interpret sort $i$ by $D_i=X_{h_{i+1}}$, interpret $S_i$ by the objects of $\mathcal P(X_{h_i})$, and interpret adjacent-sort membership by actual membership restricted to these designated <sets>. All other objects of a sort are typed <urelements>. Every <subset> of $D_i$ is a designated <set> in $D_{i+1}$, so comprehension holds for every <first-order formula>, including <first-order formulas> with quantifiers and parameters at other sorts. Two designated <sets> with the same members are equal, while the other objects have no typed members. Thus this is a full model of the typed axioms for every increasing <sequence> of levels. The extra preceding level $h_0$ gives a consistent interpretation of the bottom <set> predicate as well.
Take finitely many ambiguity sentences and let $r$ bound their highest sort before raising. Color increasing $(r+2)$-tuples $(h_0,\ldots,h_{r+1})$ by the vector of truth values of these sentences in the corresponding finite sorted structure. There are finitely many colors. The infinite <Ramsey theorem> supplies an <homogeneous set> of indices. Choose the level <sequence> from it. The sentence $\phi$ is evaluated in the window $(h_0,\ldots,h_{r+1})$, while $\phi^+$ is evaluated in the next window $(h_1,\ldots,h_{r+2})$; homogeneity makes their truth values equal. Sentences using fewer sorts simply ignore the unused final levels. Thus every finite family of ambiguity axioms has a model satisfying all the typed axioms. Apply many-sorted first-order <compactness theorem> to obtain
$$
\boxed{\operatorname{Con}(\mathrm{TSTU}+\mathrm{Typical\ Ambiguity}).}
$$
This is a relative consistency construction in the ordinary set-theoretic metatheory. Allowing urelements is essential here: skipping ranks leaves objects outside the represented <power sets>, and those objects must be permitted as <urelements>.
Back to article page
