 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 $\mathrm{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^{\ast }$ 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^{\ast }$, require them to be distinct, and impose the schemefor every formula in the Skolem language. If an elementary extension of $M^{\ast }$ 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,\dots$ 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^{\ast }$ 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^{\ast }$: whenever an existential formula with parameters from $H$ is true in $N^{\ast }$, 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 $\mathrm{Th}(M)$.

For an order automorphism $\sigma :I\to I$, defineThis 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 $\hat{\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. Uniqueness is asserted in the Skolem expansion, not for all automorphisms of its reduct.