= Solution
One useful form of the <Ehrenfeucht-Mostowski theorem> is this: for an infinite <first-order structure> $A$ and any total order $I$, there is a <first-order model> of $\operatorname{Th}(A)$ generated in a chosen <Skolem expansion> by an <order-indiscernible sequence> $(c_i)_{i\in I}$ of distinct elements. Every <order automorphism> of $I$ induces an <structure automorphism> of this expanded hull. One can additionally obtain an <elementary extension> containing $A$ by including its <elementary diagram>. Uniqueness of the induced <structure automorphism> is asserted in the <Skolem expansion>, not among arbitrary <structure automorphisms> of the reduct.
Choose a <Skolem expansion> $A^*$: for every existential <first-order formula> choose a witness <function>, satisfying $\exists y\,\varphi(y,\bar x)\Rightarrow\varphi(f_\varphi(\bar x),\bar x)$. Iterate the expansion if necessary so witnesses are available for <first-order formulas> in the resulting language. Add constants $c_i$ and require $c_i\ne c_j$ for distinct indices. For every <first-order formula> $\varphi(x_1,\ldots,x_m)$ of the expanded language and every two increasing index tuples, add
$$
\varphi(c_{i_1},\ldots,c_{i_m})\longleftrightarrow
\varphi(c_{j_1},\ldots,c_{j_m}).
$$
Together with $\operatorname{Th}(A^*)$, this is the indiscernibility theory.
Every finite fragment is satisfiable. It mentions only finitely many <first-order formulas> and index constants. Choose a countably infinite <sequence> of distinct elements of $A^*$. For each relevant arity, colour increasing tuples from that <sequence> by the finite truth vector of all <first-order formulas> of that arity in the fragment. Successive applications of the infinite <Ramsey theorem for r-sets> leave an infinite <subset> homogeneous for each of these finitely many finite colourings. Interpret the finitely many index constants by distinct elements of that <subset> in increasing enumeration order. All the required truth-value equivalences then hold, and the original structure satisfies the finite part of its own theory.
If an actual <elementary extension> of $A$ is desired, include constants for its elements and the <elementary diagram> of $A^*$. A finite fragment still contains only finitely many parameter instances; include those truth vectors in the same colourings. Thus finite satisfiability is unchanged. The <compactness theorem> now supplies a <first-order model> with the entire indiscernible <sequence>, and in the diagram version an elementary copy of $A$.
Take the <Skolem hull> of the generators, including the diagram constants when present. The witness <functions> show directly that the hull is elementary: whenever an existential <first-order formula> with hull parameters is true in the ambient <first-order model>, its Skolem witness belongs to the hull. Induction on <first-order formulas>, or the <Tarski-Vaught test>, gives elementarity. Its reduct is therefore a <first-order model> of $\operatorname{Th}(A)$. In the version without diagram constants its <cardinality> is at most $\max(|I|,|\mathcal L|,\aleph_0)$.
For an <order automorphism> $\rho:I\to I$, define
$$
\widehat\rho\bigl(t(c_{i_1},\ldots,c_{i_m})\bigr)
=t(c_{\rho(i_1)},\ldots,c_{\rho(i_m)}).
$$
This is well defined. If two terms represent the same element, express their equality as a <first-order formula> on the increasing <union> of their generator indices. Indiscernibility and preservation of the index order carry that equality to the transported terms. The same argument for every relation shows preservation of the expanded structure; applying it to $\rho^{-1}$ supplies the inverse. Every element is a term in the generators, so no other <structure automorphism> of the specified expansion can have the same action on them. Hence
$$
\boxed{\text{order automorphisms of }I\text{ extend uniquely to the generated Skolem expansion.}}
$$
For an application requiring the generators to lie in a definable infinite ordered class, impose that class predicate and its increasing-order <first-order formulas> too. The finite-fragment proof uses an increasing <sequence> in that class, so all these additional conditions are preserved. In particular the integer index order and its shift give the <structure automorphism> used in the <NFU> construction. The constants are order indiscernibles, not necessarily indiscernibles under arbitrary permutations of the index <set>.
Back to article page
