= Ultraproduct proof of the Ehrenfeucht-Mostowski theorem
Expand an infinite <first-order structure> by <Skolem functions>, choose distinct elements $b_n$, and fix a <nonprincipal ultrafilter> $\mathcal U$ on $\mathbb N$. For each finite subset $F$ of the required index order, form the <ultrapower> over $\mathbb N^F$ using the ordered <Fubini product of ultrafilters>. Pullback along coordinate projections gives coherent elementary maps by the <Łoś theorem>. In their <directed limit of elementary embeddings>, the classes of the coordinate <functions> $\mathbf n\mapsto b_{n_i}$ are distinct and form an <order-indiscernible sequence>; every <first-order formula> on increasing coordinates has the same nested <ultrafilter> test. Their <Skolem hull> gives an <Ehrenfeucht-Mostowski model>. An index-<order automorphism> sends a term in the generators to the same term in the transported generators; indiscernibility makes this well defined. Uniqueness is in the specified <Skolem expansion>, not necessarily in its reduct. If generators must respect a definable infinite order, first produce an increasing <sequence> by an <ultrapower> of finite increasing chains.
Back to article page
