Here an ultralimit in the model-theoretic sense is a model-theoretic ultralimit: start with a first-order structure, take successive ultrapowers along their diagonal elementary embeddings, and take the directed limit of elementary embeddings of that chain. The elementary chain theorem, proved by induction on formulas after identifying the embeddings with inclusions, makes every stage elementary in the limit. This definition concerns structures, rather than the topological ultrafilter limit.
We first prove the needed Frayne embedding lemma. If , every finite subset of the elementary diagram of a structure can be realized in : existentially quantify its finitely many named elements, and use elementary equivalence. Index by finite diagram fragments, choose such realizations, and extend the filter of cones requiring each diagram formula to an ultrafilter. For each , let give its chosen coordinate realizations, filling unspecified coordinates arbitrarily. The Łoś theorem shows that is an elementary embedding of into an ultrapower of . The formulas ensure injectivity.
There is a relative version: if , keep all named elements from constant in every coordinate. Each finite diagram fragment is realizable in over those parameters by elementarity, so the resulting embedding extends the diagonal embedding of into its ultrapower.
Now use alternating ultrapowers give isomorphic ultralimits. First embed into an ultrapower of . Apply the relative lemma to , embedding into an ultrapower of over its diagonal copy. Next embed into an ultrapower of over , and continue. After coherent identifications this gives
Each is an ultrapower of along its diagonal embedding, and each is an ultrapower of likewise. The two subsequences are cofinal in the same chain of elementary substructures, so their limits are the same union. Hence . No isomorphism theorem for single ultrapowers has been assumed.
The Ehrenfeucht-Mostowski theorem says that an infinite first-order structure , after Skolem expansion, has an elementarily equivalent model generated as a Skolem hull by distinct order-indiscernible sequence for any prescribed linear order . Every order automorphism of extends uniquely to an automorphism preserving this Skolem expansion. The reduct still models , but uniqueness of an automorphism in the reduct alone is not asserted. Iterate adjoining witness functions through all successively enlarged languages, so every existential formula in the final language has its own Skolem function. Write for the resulting expanded structure.
For the Ramsey theorem proof, add constants and require that they are distinct and that every two increasing tuples of the same length agree on every formula of the expanded language. Include . A finite fragment mentions finitely many formulas and finitely many indices, say of them. Choose distinct . For each arity occurring in those formulas, color the increasing tuples of natural numbers by their finite truth vectors in . Repeated applications of the infinite Ramsey theorem give an infinite subset homogeneous for all these finitely many colorings. Interpret the constants by its first elements, in their prescribed order. All the fragment's indiscernibility requirements hold. Thus compactness theorem produces a model of the whole scheme.
Let be the Skolem hull of the . Whenever an existential formula with parameters in holds in , its chosen Skolem witness belongs to . The Tarski-Vaught test, proved by the existential step of induction on formulas, therefore makes . For an order automorphism , define
To compare different term presentations, collect all their indices into one increasing tuple. Indiscernibility transfers the equality of the terms to the transported tuple, so this map is well defined. The same argument transfers every relation; it preserves all functions by construction, and the map for is its inverse. Since every hull element is a term in the generators, uniqueness follows.
For a genuinely ultraproduct proof, keep the distinct and choose a nonprincipal ultrafilter on . For each finite ordered subset , take
where is the ordered Fubini product of ultrafilters. Explicitly, a subset is large if its indicator is true after successively applying “for -almost every ” in the increasing coordinate order. Projection to any sublist has exactly that sublist's product ultrafilter. Hence for , pulling functions back along gives an elementary embedding by the Łoś theorem. These embeddings commute. Form their directed limit of elementary embeddings; each finite tuple lies in one stage, so induction on formulas makes the stage embeddings elementary.
At a stage containing , let be the class of the coordinate function . If , equality of these coordinate functions is small: for a fixed first coordinate there is only one possible equal second coordinate, and a singleton is not in . Thus . For any increasing , the truth of is the same nested ultrafilter test applied to , independent of the actual indices. This is precisely indiscernibility in the expanded language. Its Skolem hull, and the term-transport construction above, finish the second proof. Both constructions give the required model and the extended index automorphisms.
Let be a full Skolem expansion of an infinite structure , choose distinct for , and extend the cofinite filter to a nonprincipal ultrafilter on . For a finite subset of the desired index order , define the ordered Fubini product of ultrafilters on by
where means . These nested tests decide complements and preserve intersections by induction on , so is indeed an ultrafilter. For the empty set use the one-point index set and its principal ultrafilter.
Put . If , projection of coordinates induces
A truth test independent of a coordinate is unchanged by its dummy ultrafilter quantifier. Consequently pullback preserves exactly the -large subsets, proving that the map is well defined and injective. The Łoś theorem, applied to every formula rather than just to equality, proves that it is an elementary embedding. Projections compose, so these elementary maps form a coherent directed system.
Take its directed limit of elementary embeddings . Explicitly identify two stage elements when their images agree at a common larger stage, and interpret functions and relations there. For an existential formula true in the limit, its parameters and a witness occur at a common stage; elementarity then pulls truth back to the stage of the original parameters. This verifies that all stage maps into the limit are elementary.
Let be the image in this limit of the coordinate class . These elements are distinct: in , equality would require , whose inner-coordinate section is a singleton and hence not in the nonprincipal . For , the truth of any expanded-language formula on is exactly
This expression depends on the formula and the tuple length, not on the chosen increasing indices. Thus is an order-indiscernible sequence. The empty-coordinate stage embeds elementarily into .
Their Skolem hull is elementary by the witness-function argument, and an order automorphism of extends to it by transporting the generators in every term. Equality and relation preservation follow from the displayed uniform truth test, and the inverse order automorphism gives the inverse map. Therefore this proves the Ehrenfeucht-Mostowski theorem through ultrapowers and their directed limit, with no Ramsey-theoretic step.
One form of the Ehrenfeucht-Mostowski theorem says that, for every infinite first-order structure and every total order , an elementary extension contains distinct elements forming an order-indiscernible sequence. After a suitable Skolem expansion, their Skolem hull is a first-order model of , and every order automorphism of extends to a structure automorphism of that hull. If has a definable infinite linearly ordered subset , the generators may lie in and their order may agree with that definable order. Uniqueness of the extended structure automorphism is asserted in the chosen Skolem expansion, rather than for every structure automorphism of its reduct.
Here is an ultraproduct proof of the Ehrenfeucht-Mostowski theorem. First expand to with Skolem functions for all existential first-order formulas, iterating through the enlarged languages if necessary. This is done in the ordinary classical metatheory; the choice restriction in question 1 is not a restriction on this question. Fix a nonprincipal ultrafilter on .
We can obtain an infinite sequence of distinct elements in an elementary extension of by one preliminary ultrapower. For each choose a finite list of distinct elements of . Represent by the function taking the th entry when , with an arbitrary default otherwise. Distinctness holds on a cofinite set, so follows from Łoś theorem. In the definably ordered variant, first name any parameters defining , and choose each finite list increasingly inside instead; then and for . Infinitude of an ordered set supplies every finite increasing chain. This preparatory step uses no Ramsey theorem.
For a finite subset of , define the ultrafilter on by nested membership, in this order:
where means . This is the ordered Fubini product of ultrafilters. Closure under intersections and the decision between a set and its complement hold at each nested level, proving it is an ultrafilter. For take the principal ultrafilter on the one-point product. Put
If , pull a function back along the projection . A test independent of an omitted coordinate is unchanged by its ultrafilter quantifier, so projection pushes to . The induced map is therefore an elementary embedding by Łoś theorem. These maps are coherent, giving a directed system indexed by finite subsets of .
Take its directed limit of elementary embeddings . One can verify elementarity directly: representatives of a finite tuple occur at a common stage; functions and atomic relations are interpreted there. In the existential step, a witness in the limit occurs with the parameters at some later common stage, and elementarity pulls the existence statement back. Thus every embeds elementarily into , which contains an elementary copy of .
For , let be the class of the coordinate function . Projection coherence makes this independent of . If , then for each fixed the set is cofinite. The nested test therefore gives . In the ordered variant, the same argument with gives and .
For every first-order formula of the expanded language and every increasing tuple , Łoś theorem gives
The right-hand side depends on the first-order formula and tuple length, not on the indices. This proves order indiscernibility in the expanded language. Let be the Skolem hull of the generators in . The Tarski-Vaught test gives , and its reduct is a first-order model of .
An order automorphism of acts by
Indiscernibility makes this well defined: combine the finite supports of two term expressions into one increasing tuple, and apply indiscernibility to their logical equality. Applying it to relation first-order formulas proves preservation of all relations; the inverse is induced by . Every element of the hull is such a term, so the extension is unique among structure automorphisms preserving the Skolem expansion. Moreover
This proves the theorem, including its ordered version and structure automorphism conclusion, using ultrapowers and a directed limit throughout.
Expand an infinite first-order structure by Skolem functions, choose distinct elements , and fix a nonprincipal ultrafilter on . For each finite subset of the required index order, form the ultrapower over 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 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.