Ehrenfeucht-Mostowski theorem (source code)

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

If a first-order theory has an infinite model, then for every total order $I$ it has an elementary extension containing distinct <order-indiscernible sequence>[order indiscernibles] $(a_i)_{i\in I}$ whose <Skolem hull> is a model of the theory. Every order automorphism of $I$ extends uniquely to an automorphism of that hull.