Ehrenfeucht-Mostowski model

An Ehrenfeucht-Mostowski model is generated, often as a Skolem hull, by a sequence of order indiscernibles whose finite order types determine their types.

A sequence $(a_i{)}_{i\in I}$ indexed by a total order is order-indiscernible when any two increasing finite subsequences of the same length satisfy the same first-order formulas.

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 $\mathrm{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.

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.

Every first-order theory with an infinite model has models whose automorphism groups have arbitrarily large cardinality. Choose a total order with many order automorphisms and apply the Ehrenfeucht-Mostowski theorem.