Solution (source code)

= Solution

We prove the <Ehrenfeucht-Mostowski theorem> by ordered products of <ultrafilters>, without using <Ramsey's theorem>. Choose a <Skolem expansion> $M^*$ of the infinite structure and distinct elements $b_0,b_1,\ldots$. Fix a <nonprincipal ultrafilter> $U$ on $\mathbb N$.

For a finite increasing subset $F=\{i_1<\cdots<i_r\}$ of the desired index order $I$, define the ordered <Fubini product of ultrafilters> $U_F$ on $\mathbb N^F$ by
$$
A\in U_F\quad\Longleftrightarrow\quad
U n_{i_1}\ U n_{i_2}\ \cdots\ U n_{i_r}\ [(n_i)_{i\in F}\in A].
$$
The notation $U n\ P(n)$ means that the set of $n$ satisfying $P$ belongs to $U$; the leftmost quantifier is outermost. Upward closure and intersection follow successively at each coordinate, and applying complement at each step proves the <ultrafilter> dichotomy. Products are ordered; no false claim of symmetry is needed.

Put $M_F=(M^*)^{\mathbb N^F}/U_F$, with $M_\varnothing=M^*$. If $F\subseteq G$, pullback of a function by coordinate projection induces
$$
\sigma_{FG}:[f]_{U_F}\longmapsto[f\circ\operatorname{pr}_F]_{U_G}.
$$
For a cylinder condition involving only coordinates in $F$, deleting the unused <ultrafilter> quantifiers makes its membership in $U_G$ exactly its membership in $U_F$. The <Łoś theorem> therefore makes $\sigma_{FG}$ an <elementary embedding>, not merely a homomorphism. The projection identities give $\sigma_{GH}\sigma_{FG}=\sigma_{FH}$.

Take the directed limit of this system: elements from two stages are identified if their images agree at a common larger finite stage, and formulas are evaluated at such a stage. Elementary coherence makes this well-defined. It also makes each stage elementary in the limit: a formula uses finitely many parameters, and an existential witness at a later stage can be pulled back at the level of existential truth because the transition maps are elementary. Denote the limit by $N^*$.

For each $i\in I$, let $a_i$ be the limit image of the coordinate function $n_i\mapsto b_{n_i}$. These elements are distinct. For $i<j$, after fixing $n_i$, equality $b_{n_i}=b_{n_j}$ holds for at most one $n_j$, a set not in $U$; hence equality fails in the two-coordinate <ultrapower> and therefore in the limit.

For any increasing $i_1<\cdots<i_r$, Łoś evaluates
$$
N^*\models\varphi(a_{i_1},\ldots,a_{i_r})
\quad\Longleftrightarrow\quad
U n_1\cdots U n_r\ [M^*\models\varphi(b_{n_1},\ldots,b_{n_r})].
$$
The right-hand side depends on the formula and the number of increasing coordinates, not their particular indices. Thus $(a_i)_{i\in I}$ is order-indiscernible for every formula of the expanded language simultaneously; no preliminary homogeneous thinning is used. If elements of $M$ were named before expanding, the same computation gives indiscernibility over those names and the initial stage embeds the original structure into the limit.

The <Skolem hull> of these generators is elementary by the witness property. Transporting the generators by any <order automorphism> of $I$ transports every term, with well-definedness and relation preservation supplied by the formula equivalence just proved. The inverse transport supplies an inverse automorphism. \b[The ordered-ultrapower construction gives the full Ehrenfeucht–Mostowski model and its <order automorphisms> without <Ramsey's theorem>.]