= Solution
A useful form of the <Ehrenfeucht-Mostowski theorem> says that, for an infinite <first-order structure> $M$ and any total order $I$, there is a model of $\operatorname{Th}(M)$ generated as a <Skolem hull> by distinct order indiscernibles $(a_i)_{i\in I}$. Every <order automorphism> of $I$ extends uniquely to an <automorphism> of the specified <Skolem expansion> of that hull. The model can be obtained inside an <elementary extension> of a <Skolem expansion> of $M$; the generated hull itself need not contain $M$.
Choose a <Skolem expansion> $M^*$ by iteratively adjoining witness functions: for each existential formula in the current language choose a function returning a witness whenever one exists, with an arbitrary value otherwise. Repeat for countably many rounds. Every formula in the final language uses finitely many symbols, so has a witness function from a later round. Thus the expansion is Skolemized for its own formulas, as required for elementarity of its hull. Add constants $a_i$ for $i\in I$ to the complete theory of $M^*$, require them to be distinct, and impose the scheme
$$
\varphi(a_{i_1},\ldots,a_{i_n})\longleftrightarrow\varphi(a_{j_1},\ldots,a_{j_n})
\quad(i_1<\cdots<i_n,\ j_1<\cdots<j_n)
$$
for every formula in the Skolem language. If an <elementary extension> of $M^*$ is desired, also add its <elementary diagram> with separate names for its elements.
Every finite part of this theory is satisfiable. Choose infinitely many distinct elements $b_0,b_1,\ldots$ of $M$. For each of the finitely many arities in that fragment, color increasing index tuples by the finite vector of truth values of the formulas occurring. Repeated applications of the infinite Ramsey theorem give an infinite <subset> on which all these vectors are constant. Interpret the finitely many $a_i$ in increasing-index order from that <subset>. This satisfies the finite indiscernibility requirements and distinctness, while the <elementary diagram> is satisfied by the named original structure. The <compactness theorem> gives a structure $N^*$ satisfying the whole theory.
Let $H$ be the closure of the $a_i$ under the <Skolem functions>, including nullary ones. It is elementary in $N^*$: whenever an existential formula with parameters from $H$ is true in $N^*$, its Skolem witness lies in $H$. This is the <Tarski-Vaught test>, whose proof is <induction> on formulas, using precisely this witness property for the existential step. Hence the reduct of $H$ is a model of $\operatorname{Th}(M)$.
For an <order automorphism> $\sigma:I\to I$, define
$$
\widehat\sigma\bigl(t(a_{i_1},\ldots,a_{i_n})\bigr)=t(a_{\sigma(i_1)},\ldots,a_{\sigma(i_n)}).
$$
This is well-defined. If two terms denote the same element, write their equality as a formula on the combined increasing tuple of their indices; indiscernibility preserves that formula after transport by $\sigma$. The same argument preserves every relation and function. Applying $\sigma^{-1}$ gives the inverse, so $\widehat\sigma$ is an <automorphism>. Since all elements are terms in the generators, it is the unique <automorphism> of this <Skolem expansion> extending $a_i\mapsto a_{\sigma(i)}$. This proves the theorem.
One may require the indiscernibles to lie in any specified infinite <sequence> of the starting structure, or to satisfy additional finite-tuple properties holding along that <sequence>: the same finite satisfiability proof chooses its homogeneous <subsequence> there. This strengthened form is what the rank-domain construction of <NFU> uses. \b[Uniqueness is asserted in the <Skolem expansion>, not for all <automorphisms> of its reduct.]
Back to article page
