Ehrenfeucht-Mostowski theorem (source code)

= Ehrenfeucht-Mostowski theorem
{c}
{wiki=Ehrenfeucht–Mostowski_theorem}

Let $M$ be an infinite <first-order structure> and $I$ a <total order>. After choosing a <Skolem expansion> of $M$, an <elementary extension> contains distinct elements $(a_i)_{i\in I}$ forming an <order-indiscernible sequence> in that expanded language. Their <Skolem hull> is an <elementary substructure> in the expanded language, and its reduct is a <first-order model> of $\operatorname{Th}(M)$. Every <order automorphism> of $I$ extends uniquely to a <structure automorphism> of the hull preserving the chosen <Skolem expansion>, by transporting terms in the generators.

Uniqueness need not hold among all <structure automorphisms> of the reduct. For an infinite structure in the pure <logical equality> language, take two distinct nullary <Skolem function> values $c_0,c_1$ in the hull. For an infinite <order-indiscernible sequence>, neither can equal a generator: the expanded formula $x=c_j$ would otherwise hold at every generator, contradicting their distinctness. Swapping $c_0,c_1$ fixes every generator and preserves the pure <logical equality> reduct, while failing to preserve the <Skolem expansion>. Thus the identity <order automorphism> already has two extensions in that reduct.