= Solution
One form of the <Ehrenfeucht-Mostowski theorem> says that, for every infinite <first-order structure> $M$ and every <total order> $I$, an <elementary extension> contains distinct elements $(a_i)_{i\in I}$ forming an <order-indiscernible sequence>. After a suitable <Skolem expansion>, their <Skolem hull> is a <first-order model> of $\operatorname{Th}(M)$, and every <order automorphism> of $I$ extends to a <structure automorphism> of that hull. If $M$ has a definable infinite linearly ordered subset $P$, the generators may lie in $P$ and their order may agree with that definable order. Uniqueness of the extended <structure automorphism> is asserted in the chosen <Skolem expansion>, rather than for every <structure automorphism> of its reduct.
Here is an <ultraproduct proof of the Ehrenfeucht-Mostowski theorem>. First expand $M$ to $M^+$ with <Skolem functions> for all existential <first-order formulas>, iterating through the enlarged languages if necessary. This is done in the ordinary classical metatheory; the choice restriction in question 1 is not a restriction on this question. Fix a <nonprincipal ultrafilter> $\mathcal U$ on $\mathbb N$.
We can obtain an infinite <sequence> of distinct elements $b_0,b_1,\ldots$ in an <elementary extension> $M_0$ of $M^+$ by one preliminary <ultrapower>. For each $n\geq1$ choose a finite list of $n$ distinct elements of $M^+$. Represent $b_j$ by the <function> taking the $j$th entry when $n>j$, with an arbitrary default otherwise. Distinctness holds on a <cofinite set>, so follows from <Łoś theorem>. In the definably ordered variant, first name any parameters defining $P$, and choose each finite list increasingly inside $P$ instead; then $M_0\models P(b_j)$ and $b_j<b_k$ for $j<k$. Infinitude of an ordered <set> supplies every finite increasing chain. This preparatory step uses no <Ramsey theorem>.
For a finite subset $F=\{i_1<\cdots<i_r\}$ of $I$, define the <ultrafilter> $\mathcal U_F$ on $\mathbb N^F$ by nested membership, in this order:
$$
E\in\mathcal U_F\quad\Longleftrightarrow\quad(\mathcal U n_{i_1})\cdots(\mathcal U n_{i_r})\,[\mathbf n\in E],
$$
where $(\mathcal U n)\,Q(n)$ means $\{n:Q(n)\}\in\mathcal U$. This is the ordered <Fubini product of ultrafilters>. Closure under intersections and the decision between a <set> and its complement hold at each nested level, proving it is an <ultrafilter>. For $F=\varnothing$ take the <principal ultrafilter> on the one-point product. Put
$$
N_F=M_0^{\mathbb N^F}/\mathcal U_F.
$$
If $F\subseteq G$, pull a <function> back along the projection $\mathbb N^G\to\mathbb N^F$. A test independent of an omitted coordinate is unchanged by its <ultrafilter> quantifier, so projection pushes $\mathcal U_G$ to $\mathcal U_F$. The induced map $N_F\to N_G$ is therefore an <elementary embedding> by <Łoś theorem>. These maps are coherent, giving a directed system indexed by finite subsets of $I$.
Take its <directed limit of elementary embeddings> $N$. One can verify elementarity directly: representatives of a finite tuple occur at a common stage; <functions> and atomic relations are interpreted there. In the existential step, a witness in the limit occurs with the parameters at some later common stage, and elementarity pulls the existence statement back. Thus every $N_F$ embeds elementarily into $N$, which contains an elementary copy of $M^+$.
For $i\in F$, let $a_i$ be the class of the coordinate <function> $\mathbf n\mapsto b_{n_i}$. Projection coherence makes this independent of $F$. If $i<j$, then for each fixed $n_i$ the <set> $\{n_j:n_j\ne n_i\}$ is cofinite. The nested test therefore gives $a_i\ne a_j$. In the ordered variant, the same argument with $n_j>n_i$ gives $P(a_i)$ and $a_i<a_j$.
For every <first-order formula> $\varphi$ of the expanded language and every increasing tuple $i_1<\cdots<i_r$, <Łoś theorem> gives
$$
N\models\varphi(a_{i_1},\ldots,a_{i_r})\quad\Longleftrightarrow\quad(\mathcal U n_1)\cdots(\mathcal U n_r)\,[M_0\models\varphi(b_{n_1},\ldots,b_{n_r})].
$$
The right-hand side depends on the <first-order formula> and tuple length, not on the indices. This proves order indiscernibility in the expanded language. Let $H$ be the <Skolem hull> of the generators in $N$. The <Tarski-Vaught test> gives $H\prec N$, and its reduct is a <first-order model> of $\operatorname{Th}(M)$.
An <order automorphism> $\pi$ of $I$ acts by
$$
t(a_{i_1},\ldots,a_{i_r})\longmapsto t(a_{\pi(i_1)},\ldots,a_{\pi(i_r)}).
$$
Indiscernibility makes this well defined: combine the finite supports of two term expressions into one increasing tuple, and apply indiscernibility to their <logical equality>. Applying it to relation <first-order formulas> proves preservation of all relations; the inverse is induced by $\pi^{-1}$. Every element of the hull is such a term, so the extension is unique among <structure automorphisms> preserving the <Skolem expansion>. Moreover
$$
\boxed{|H|\leq\max(|I|,|L|,\aleph_0),\quad\text{and }|H|=|I|\text{ if }|I|\geq|L|+\aleph_0.}
$$
This proves the theorem, including its ordered version and <structure automorphism> conclusion, using <ultrapowers> and a directed limit throughout.
Back to article page
