Codex @codex  0

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.

An order automorphism of a total order $(I,<)$ is a bijection $\pi :I\to I$ such that $i<j$ if and only if $\pi (i)<\pi (j)$. Composition and inverses are again order automorphisms. Transporting the indices of an order-indiscernible sequence by such a map preserves every first-order formula on increasing finite tuples.

One useful form of the Ehrenfeucht-Mostowski theorem is this: for an infinite first-order structure $A$ and any total order $I$, there is a first-order model of $\mathrm{Th}(A)$ generated in a chosen Skolem expansion by an order-indiscernible sequence $(c_i{)}_{i\in I}$ of distinct elements. Every order automorphism of $I$ induces an structure automorphism of this expanded hull. One can additionally obtain an elementary extension containing $A$ by including its elementary diagram. Uniqueness of the induced structure automorphism is asserted in the Skolem expansion, not among arbitrary structure automorphisms of the reduct.

Choose a Skolem expansion $A^{\ast }$: for every existential first-order formula choose a witness function, satisfying $\exists y\phi (y,\bar{x})\Rightarrow \phi (f_{\phi }(\bar{x}),\bar{x})$. Iterate the expansion if necessary so witnesses are available for first-order formulas in the resulting language. Add constants $c_i$ and require $c_i\ne c_j$ for distinct indices. For every first-order formula $\phi (x_1,\dots ,x_m)$ of the expanded language and every two increasing index tuples, addTogether with $\mathrm{Th}(A^{\ast })$, this is the indiscernibility theory.

Every finite fragment is satisfiable. It mentions only finitely many first-order formulas and index constants. Choose a countably infinite sequence of distinct elements of $A^{\ast }$. For each relevant arity, colour increasing tuples from that sequence by the finite truth vector of all first-order formulas of that arity in the fragment. Successive applications of the infinite Ramsey theorem for r-sets leave an infinite subset homogeneous for each of these finitely many finite colourings. Interpret the finitely many index constants by distinct elements of that subset in increasing enumeration order. All the required truth-value equivalences then hold, and the original structure satisfies the finite part of its own theory.

If an actual elementary extension of $A$ is desired, include constants for its elements and the elementary diagram of $A^{\ast }$. A finite fragment still contains only finitely many parameter instances; include those truth vectors in the same colourings. Thus finite satisfiability is unchanged. The compactness theorem now supplies a first-order model with the entire indiscernible sequence, and in the diagram version an elementary copy of $A$.

Take the Skolem hull of the generators, including the diagram constants when present. The witness functions show directly that the hull is elementary: whenever an existential first-order formula with hull parameters is true in the ambient first-order model, its Skolem witness belongs to the hull. Induction on first-order formulas, or the Tarski-Vaught test, gives elementarity. Its reduct is therefore a first-order model of $\mathrm{Th}(A)$. In the version without diagram constants its cardinality is at most $\max (|I|,|\mathcal{L}|,{\aleph }_0)$.

For an order automorphism $\rho :I\to I$, defineThis is well defined. If two terms represent the same element, express their equality as a first-order formula on the increasing union of their generator indices. Indiscernibility and preservation of the index order carry that equality to the transported terms. The same argument for every relation shows preservation of the expanded structure; applying it to ${\rho }^{-1}$ supplies the inverse. Every element is a term in the generators, so no other structure automorphism of the specified expansion can have the same action on them. HenceFor an application requiring the generators to lie in a definable infinite ordered class, impose that class predicate and its increasing-order first-order formulas too. The finite-fragment proof uses an increasing sequence in that class, so all these additional conditions are preserved. In particular the integer index order and its shift give the structure automorphism used in the NFU construction. The constants are order indiscernibles, not necessarily indiscernibles under arbitrary permutations of the index set.

We give a relative consistency proof: a model of ZFC yields a model of NFU. This proves the requested consistency relative to the usual background set theory; it does not claim the optimal, much weaker consistency bound for bare NFU.

Recall that New Foundations with urelements has a unary set predicate $S$, atoms without members, extensionality restricted to sets, and comprehension for every stratified formula. Stratification assigns integer types to variables, with equal types at equality and adjacent types at membership. We construct a model of simple typed set theory with atoms with a type-shifting automorphism, then identify its types using that automorphism.

Start with a model of ZFC and a Skolem expansion of it. By the compactness theorem there is a model $N$ of the same expanded theory with an increasing integer-indexed order-indiscernible sequence of ordinals $⟨c_i:i\in \mathbb{Z}⟩$, all above $\omega$. Here is the finite-satisfiability argument. A finite fragment names only finitely many $c_i$ and asks for equal truth values of finitely many formulas on increasing tuples. In the starting model choose an infinite increasing sequence of ordinals above $\omega$. Colour its finite subsets by these truth vectors, successively treating each tuple length. The Ramsey's theorem supplies an infinite homogeneous subsequence for the finitely many colours and arities. Its first required number of elements interprets all named $c_i$ and satisfies that fragment. Compactness gives the entire sequence. This argument works for the countable expanded language because each fragment uses only finitely many formulas.

Replace $N$ by the Skolem hull of the $c_i$. The mapis well defined by indiscernibility: equal terms remain equal after shifting their increasing lists of indices. The same argument preserves every formula. Shifting indices backwards gives its inverse, so $j$ is an automorphism of the hull, and $j(c_i)=c_{i+1}>c_i$. The Skolem hull is elementary by its witness functions. This is a concrete Ehrenfeucht-Mostowski model; it is not an elementary class self-embedding of the actual well-founded universe.

Set $D_i=V_{c_i}^N$, interpreted externally as the objects belonging to that internal rank segment, for every integer $i$. At type $i$ declareand define adjacent-type membership byThe members of a type-$i+1$ set are exactly a subset of $D_i$; a type-$i+1$ atom has no ${\epsilon }_i$-members. Every internal subset of $D_i$ is an object of $D_{i+1}$, since $c_{i+1}>c_i$. Extensionality for sets is inherited from $N$. For a typed formula involving finitely many types, restrict its quantifiers to the corresponding internal $D_k$ and express each $S_k$ and ${\epsilon }_k$ by the displayed definitions. Separation in $N$ gives the required subset of $D_i$, which represents its comprehension at type $i+1$. This verifies the typed theory even though many higher-type objects are atoms. The automorphism $j$ carries $D_i,S_i,{\epsilon }_i$ to the next type.

On domain $D_0$, define $S(x)=S_0(x)$ andIf $S(y)$ is false, $S_1(j(y))$ is false, so $y$ has no $E$-members. For sets $y,z$, equality of their $E$-extensions gives equality of the typed sets $j(y),j(z)$ and hence $y=z$. To check stratified comprehension, translate a variable of type $k$ into $j^k(x)$. The automorphism laws make membership and equality translate exactly. A stratified predicate on a variable of type zero defines a typed subset $B$ of $D_0$, represented by a set at type one. Then $b=j^{-1}(B)\in D_0$ has $E$-extension exactly that predicate. A uniform type shift handles any other type assigned to the comprehended variable. The resulting untyped structure is a model of NFU.

We prove the Ehrenfeucht-Mostowski theorem by ultraproducts, with no application of Ramsey theorem. Expand the infinite structure $M$ by Skolem functions, choose distinct elements $a_0,a_1,\dots$, and choose a nonprincipal ultrafilter $D$ on $\omega$. Let $I$ be the desired total index order and put $J={\omega }^I$.

For every finite ordered subset $F=\{i_1<\cdots <i_n\}$, define an ultrafilter $D_F$ on ${\omega }^F$ by the ordered Fubini product of ultrafilters: a set $B$ belongs to $D_F$ exactly whenHere $(Dm)\psi (m)$ means $\{m:\psi (m)\}\in D$, with the quantifiers nested in the displayed order. The resulting collection is an ultrafilter, by induction using the ultrafilter laws for negation and conjunction. For $F\subseteq H$, the inverse image of $B\subseteq {\omega }^F$ under coordinate projection belongs to $D_H$ exactly when $B\in D_F$: quantifiers on unused coordinates leave a truth value unchanged.

Consequently there is a well-defined ultrafilter on the Boolean algebra of finite-coordinate cylinders in $J$, declaring a cylinder large by this test. Coherence proves finite intersection closure and ensures that the empty cylinder is not large. Extend its generated filter to an ultrafilter $U$ on all subsets of $J$. Form the ultrapower $N=(M^{\ast }{)}^J/U$, and for $i\in I$ let $b_i$ be the class of $s\mapsto a_{s(i)}$.

If $i\ne j$, the coordinate equality test belongs to no corresponding two-coordinate product ultrafilter: for every value of the outer coordinate, the inner equality set is a singleton, excluded by nonprincipality. Hence the $b_i$ are distinct. For any first-order formula $\phi (x_1,\dots ,x_n)$ and any $i_1<\cdots <i_n$, the Łoś theorem givesThe right side is independent of the actual increasing index tuple, so the $b_i$ form an order-indiscernible sequence. Constant functions embed $M^{\ast }$ elementarily into $N$. Take the Skolem hull of the generators. The Tarski-Vaught test gives an elementary substructure, and transporting terms along an index-order automorphism gives a well-defined automorphism of the hull, with inverse obtained by transporting along the inverse index automorphism. Equality of term representations is preserved by indiscernibility. This is the indiscernible and automorphism conclusion of Ehrenfeucht–Mostowski, obtained entirely from ultrafilters and Łoś's theorem. The ordered Fubini products need not be symmetric; order indiscernibility is exactly what their coherence supplies.

For the Ehrenfeucht-Mostowski theorem, start with an infinite structure $M$ and a total order $I$. Choose a Skolem expansion $M^{\ast }$, and adjoin constants $c_i$ for $i\in I$. Require the elementary diagram of $M^{\ast }$, distinctness of these new constants, and the order-indiscernible sequence schema: any two increasing tuples of the $c_i$ of the same length satisfy the same first-order formulas in the expanded language. Every finite fragment mentions finitely many new constants and finitely many first-order formulas. Enumerate a countably infinite subset of $M$. For each of the finitely many first-order formulas, color its increasing tuples by its truth value in $M^{\ast }$, including whatever fixed parameters occur in the fragment. Successive applications of the infinite Ramsey theorem leave an infinite subset homogeneous for all these colorings. Assign the finitely many new constants to distinct elements of this subset in their index order. Their finite indiscernibility requirements and the elementary diagram are then simultaneously satisfied.

The compactness theorem supplies an elementary extension $N^{\ast }$ containing the required distinct indiscernibles. Their Skolem hull is an elementary substructure: an existential first-order formula true of its elements has its chosen Skolem-function witness in the hull, so the Tarski-Vaught test applies. Any order automorphism $\sigma$ of $I$ acts on this hull byIndiscernibility makes this well defined, since every equality of two term representations is preserved. The same argument preserves every first-order formula; the inverse is given by ${\sigma }^{-1}$. Thus it is an automorphism, uniquely determined in the language of the chosen Skolem expansion by its values on the generators. This proves both the indiscernible-model and automorphism forms of the Ehrenfeucht-Mostowski theorem. Uniqueness is not claimed for automorphisms of the reduct which need not preserve the chosen Skolem functions.

For simple typed set theory with atoms, write $S_i$ for the set predicate at sort $i$. Members have sort one lower; urelements have no typed members, extensionality applies to sets, and every well-typed first-order formula defines a set at the next sort. Typical ambiguity adds $\varphi \leftrightarrow {\varphi }^{+}$ for each closed sentence, where $+$ raises every sort by one. We prove finite satisfiability using Ramsey theorem, rather than assuming that adjacent sorts have the same cardinality.

Let $X_n=V_{\omega +2n}$. If $n<m$, then $\mathcal{P}(X_n)\subseteq X_m$. For increasing integers $h_0<h_1<h_2<\cdots$, interpret sort $i$ by $D_i=X_{h_{i+1}}$, interpret $S_i$ by the objects of $\mathcal{P}(X_{h_i})$, and interpret adjacent-sort membership by actual membership restricted to these designated sets. All other objects of a sort are typed urelements. Every subset of $D_i$ is a designated set in $D_{i+1}$, so comprehension holds for every first-order formula, including first-order formulas with quantifiers and parameters at other sorts. Two designated sets with the same members are equal, while the other objects have no typed members. Thus this is a full model of the typed axioms for every increasing sequence of levels. The extra preceding level $h_0$ gives a consistent interpretation of the bottom set predicate as well.

Take finitely many ambiguity sentences and let $r$ bound their highest sort before raising. Color increasing $(r+2)$-tuples $(h_0,\dots ,h_{r+1})$ by the vector of truth values of these sentences in the corresponding finite sorted structure. There are finitely many colors. The infinite Ramsey theorem supplies an homogeneous set of indices. Choose the level sequence from it. The sentence $\varphi$ is evaluated in the window $(h_0,\dots ,h_{r+1})$, while ${\varphi }^{+}$ is evaluated in the next window $(h_1,\dots ,h_{r+2})$; homogeneity makes their truth values equal. Sentences using fewer sorts simply ignore the unused final levels. Thus every finite family of ambiguity axioms has a model satisfying all the typed axioms. Apply many-sorted first-order compactness theorem to obtainThis is a relative consistency construction in the ordinary set-theoretic metatheory. Allowing urelements is essential here: skipping ranks leaves objects outside the represented power sets, and those objects must be permitted as urelements.

The Ehrenfeucht-Mostowski theorem asserts that an infinite first-order structure has, for any prescribed total order $I$, an elementary extension containing distinct order-indiscernibles $(c_i{)}_{i\in I}$. After a Skolem expansion, the Skolem hull of those generators is a model of the original complete theory. Every order automorphism of $I$ extends to a unique automorphism of this specified Skolem hull in the expanded language.

Choose a Skolem expansion $M^{\ast }$ of the original infinite structure: for each existential formula, select a witness function, including nullary functions when needed. Add constants $c_i$ for $i\in I$ and the elementary diagram of a structure of $M^{\ast }$, using separate names for its elements. Require $c_i\ne c_j$ for distinct indices, and for each formula $\phi$ in the Skolem language requirewhenever both index tuples are strictly increasing. These are the order-indiscernible sequence requirements.

Every finite fragment is satisfiable in $M^{\ast }$. Choose a countably infinite sequence of distinct elements of $M^{\ast }$. The fragment mentions only finitely many formulas and arities. Color increasing $k$-tuples of that sequence by the finite vector of truth values of its relevant $k$-ary formulas. The Ramsey theorem supplies an infinite homogeneous subsequence; repeat for the finitely many arities. Assign the finitely many named $c_i$ to distinct elements of the final homogeneous subsequence in increasing index order. The fixed finite part of the elementary diagram of a structure already holds in $M^{\ast }$. By the compactness theorem proved in Question 5, the full set of requirements has a model $N^{\ast }$, giving the required elementary extension and order-indiscernible sequence.

Let $H$ comprise all values of Skolem-language terms in finitely many $c_i$. It is closed under the witness functions. If $N^{\ast }\models \exists x\psi (x,\bar{h})$ for parameters in $H$, the specified witness function supplies a witness in $H$. Induction on formulas therefore gives $H⪯N^{\ast }$; its reduct is a model of $\mathrm{Th}(M)$. For infinite $I$, its cardinality is at most $\max (|I|,|L^{\ast }|,{\aleph }_0)$ and at least $|I|$.

For an order automorphism $\alpha :I\to I$, defineRewrite any finite list of indices in increasing order, allowing a term to repeat or omit variables. The order-indiscernible sequence property transfers every equality between terms and every relation among their values, making this definition well defined and elementary. Applying ${\alpha }^{-1}$ gives its inverse. All of $H$ is generated by the $c_i$ and the named Skolem functions, so an automorphism extending $\alpha$ must have precisely this action. Thus $\boxed{\mathrm{Aut}(I)\hookrightarrow \mathrm{Aut}(H^{\ast })}$, with uniqueness in the Skolem expansion. This uniqueness need not hold in the unexpanded reduct.

The Ehrenfeucht-Mostowski theorem says that an infinite first-order structure $M$, after Skolem expansion, has an elementarily equivalent model generated as a Skolem hull by distinct order-indiscernible sequence $(a_i{)}_{i\in I}$ for any prescribed linear order $I$. Every order automorphism of $I$ extends uniquely to an automorphism preserving this Skolem expansion. The reduct still models $\mathrm{Th}(M)$, 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 $M^{\ast }$ for the resulting expanded structure.

For the Ramsey theorem proof, add constants $c_i$ 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 $\mathrm{Th}(M^{\ast })$. A finite fragment mentions finitely many formulas and finitely many indices, say $r$ of them. Choose distinct $b_n\in M$. For each arity occurring in those formulas, color the increasing tuples of natural numbers by their finite truth vectors in $M^{\ast }$. Repeated applications of the infinite Ramsey theorem give an infinite subset homogeneous for all these finitely many colorings. Interpret the $r$ constants by its first $r$ elements, in their prescribed order. All the fragment's indiscernibility requirements hold. Thus compactness theorem produces a model $N^{\ast }$ of the whole scheme.

Let $H$ be the Skolem hull of the $c_i$. Whenever an existential formula with parameters in $H$ holds in $N^{\ast }$, its chosen Skolem witness belongs to $H$. The Tarski-Vaught test, proved by the existential step of induction on formulas, therefore makes $H\prec N^{\ast }$. For an order automorphism $\rho :I\to I$, defineTo 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 ${\rho }^{-1}$ is its inverse. Since every hull element is a term in the generators, uniqueness follows.

For a genuinely ultraproduct proof, keep the distinct $b_n$ and choose a nonprincipal ultrafilter $\mathcal{U}$ on $\mathbb{N}$. For each finite ordered subset $F\subset I$, takewhere ${\mathcal{U}}_F$ is the ordered Fubini product of ultrafilters. Explicitly, a subset $A\subseteq {\mathbb{N}}^F$ is large if its indicator is true after successively applying “for $\mathcal{U}$-almost every $n_i$” in the increasing coordinate order. Projection to any sublist has exactly that sublist's product ultrafilter. Hence for $F\subseteq G$, pulling functions back along ${\mathbb{N}}^G\to {\mathbb{N}}^F$ gives an elementary embedding $M_F\to M_G$ 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 $i$, let $a_i$ be the class of the coordinate function $\mathbf{n}\mapsto b_{n_i}$. If $i<j$, 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 $\mathcal{U}$. Thus $a_i\ne a_j$. For any increasing $i_1<\cdots <i_r$, the truth of $\phi (a_{i_1},\dots ,a_{i_r})$ is the same nested ultrafilter test applied to $\phi (b_{n_1},\dots ,b_{n_r})$, 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.

A useful precise form of the Ehrenfeucht-Mostowski theorem is this: for an infinite structure $M$ and any linear order $I$, a model of $\mathrm{Th}(M)$ can be generated as a Skolem hull by distinct order indiscernibles $(a_i{)}_{i\in I}$. Every order automorphism of $I$ extends to an automorphism of that hull in the chosen Skolem language. One may first name all elements of $M$, giving an elementary extension containing the original structure. The generation and uniqueness assertions concern this specified expansion, not arbitrary automorphisms of its reduct.

Choose a Skolem expansion $M^{\ast }$: for each existential formula add a function selecting a witness whenever one exists. Introduce constants $c_i$ for $i\in I$. Take the theory of $M^{\ast }$, distinctness of these constants, and all equivalencesThe formulas here are in the fixed expanded language, without the newly added $c_i$ as extra parameters. If naming $M$, use its complete elementary diagram and allow those original names in the formulas.

Every finite fragment has a model by Ramsey's theorem. Only finitely many formulas and constants occur. Take a sequence of distinct elements of $M$. For each arity appearing, color the increasing tuples from this sequence by the finite vector of truth values of all formulas of that arity. Successive Ramsey thinning gives an infinite subset homogeneous for each of these finitely many colorings. Assign the finitely many constants in increasing order to distinct elements of this subset. This satisfies every displayed equivalence in the fragment; the original theory is satisfied because the underlying structure remains $M^{\ast }$. Compactness now gives a model of the full theory, with the required order-indiscernible sequence.

The substructure generated by the constants under the Skolem functions is elementary: any existential formula with parameters which are terms in the generators has its Skolem witness in that same hull. If $g$ is an order automorphism of $I$, defineIndiscernibility makes this well-defined, by applying it to the equation between any two term representations using the increasing tuple of all their indices. The same argument preserves every relation and function; $g^{-1}$ supplies the inverse. It is unique in the generated Skolem structure. This completes the Ramsey proof, rather than stopping at the existence of indiscernibles.

For simple typed set theory with atoms, use sorts $D_0,D_1,\dots$ and membership only from $D_i$ to $D_{i+1}$. A set predicate distinguishes sets from atoms, extensionality compares sets of the same positive type, and comprehension produces in type $i+1$ every subset of $D_i$ defined by a well-typed formula. Atoms have no members. First-order models use Henkin semantics; they are not required to have their next domain equal to the full external power set. Typical ambiguity is the schema $\varphi \leftrightarrow {\varphi }^{+}$ for each closed sentence, where every sort index in ${\varphi }^{+}$ is raised by one.

We show finite satisfiability of this entire typed theory with ambiguity. Choose a list of ranks ${\rho }_0<{\rho }_1<\cdots$ above $\omega$, spaced by at least two. For a finite increasing selection of ranks $r_{-1}<r_0<\cdots <r_m$, letwhere $S_i$ is the set of objects declared to be sets at type $i$. Membership from $D_i$ to $D_{i+1}$ is ordinary membership restricted to objects of $S_{i+1}=\mathcal{P}(D_i)$; all other type-$i+1$ objects are atoms. The spacing puts $\mathcal{P}(D_i)$ inside $D_{i+1}$. Thus comprehension and set extensionality hold exactly, and atoms have no typed members. There are infinitely many objects at every visible type, so any usual typed infinity requirement also holds.

The auxiliary rank $r_{-1}$ provides a uniform interpretation if a set predicate is allowed at type zero; no type-minus-one domain is used in the theory. This avoids artificially declaring all type-zero objects to be atoms, which would not be invariant under type-raising. If the language has no type-zero set predicate, simply ignore this auxiliary interpretation.

A finite set of ambiguity instances uses finitely many closed sentences of bounded highest type, say at most $m$. Color increasing $(m+2)$-tuples of ranks by their finite truth vector in the structure with visible domains $D_0,\dots ,D_m$ and the auxiliary preceding rank. Ramsey's theorem gives an infinite homogeneous rank set. Choose $m+3$ consecutive ranks from it and build the hierarchy on all these ranks. The first window evaluates each original sentence; shifting the window one place evaluates its uniform type-raise. Homogeneity makes the truth vectors equal. All finite typed axioms and the selected ambiguity instances therefore hold together. Choosing $m$ large enough covers every sort needed by the finite fragment. Many-sorted compactness, equivalently ordinary first-order compactness after encoding sorts, yieldsThis is a model existence argument in the ambient set theory; no equality of adjacent type cardinalities is claimed. The gaps between ranks supply atoms, and the ambiguity is about truth of sentences, not a bijection between domains.

For the Ehrenfeucht-Mostowski theorem, let $M$ be an infinite first-order structure and $I$ any linear order. Choose a full Skolem expansion $M^{\ast }$: add witness functions for existential formulas, repeat in the expanded languages, and take their union. We will construct a model of its theory containing distinct generators $c_i$, $i\in I$, forming an order-indiscernible sequence.

Adjoin the elementary diagram of $M^{\ast }$, the inequalities $c_i\ne c_j$ for $i\ne j$, and for every expanded-language formula $\varphi (x_1,\dots ,x_r)$ and every two increasing $r$-tuples of indices, the sentencesEvery finite subcollection is satisfiable in $M^{\ast }$. To prove this, choose a countably infinite sequence of distinct elements of $M$, and for each of the finitely many relevant arities color its increasing index tuples by the finite vector of truth values of the formulas of that arity. Repeated applications of the Ramsey's theorem give an infinite subsequence homogeneous for all these finitely many finite colorings. Interpret the finitely many mentioned $c_i$ by its elements in their index order. All indiscernibility and distinctness constraints hold, and the finite diagram fragment holds because the ambient structure is still $M^{\ast }$.

By compactness theorem, a model $N^{\ast }$ of the full enlarged theory exists. Its Skolem hull $H$ generated by the $c_i$ is elementary: whenever an existential formula with parameters in $H$ holds in $N^{\ast }$, its chosen witness function returns a value in $H$, so the Tarski-Vaught test applies. Its reduct is a model of $\mathrm{Th}(M)$. If the index order has size $\kappa$, the hull has size at most $\kappa +|L|+{\aleph }_0$, and it contains $|I|$ distinct generators.

Every order automorphism $h$ of $I$ induces the automorphismTo check well-definedness, write any two terms being compared over the same increasing list of their generators. Their equality is an expanded-language formula; indiscernibility of the order-indiscernible sequence preserves its truth under $h$. The same argument preserves each relation, and the term construction preserves the functions. Applying $h^{-1}$ gives the inverse. The extension is unique in the specified Skolem language since every hull element is a term in the generators; no uniqueness among all automorphisms of the reduct is being asserted. This proves the Ehrenfeucht-Mostowski theorem, including its usual automorphism consequence.

For simple typed set theory with atoms, use sorts $0,1,\dots$, predicates $S_i$ for sets, and typed membership from sort $i$ to sort $i+1$. Atoms have no members, extensionality compares sets, and every well-typed formula defines a set of the next sort. Typical ambiguity is the schema $\varphi \leftrightarrow {\varphi }^{+}$ for every closed typed sentence, where the superscript raises all types by one.

Here are concrete full typed models before imposing the ambiguity schema. Choose increasing natural numbers $n_{-1}<n_0<n_1<\cdots$ and setThe auxiliary $D_{-1}$ merely interprets the set predicate at the lowest sort. Define typed membership byThen the other objects of $D_{i+1}$ are atoms, regardless of their old membership. Every subset of $D_i$ has its representative in $S_{i+1}$, giving comprehension even for formulas with higher-sort quantifiers and parameters. Extensionality holds for the set representatives and atoms have no typed members. The rank gaps leave infinitely many atoms at each sort, and all sorts are infinite.

Consider finitely many ambiguity instances with unraised sentences ${\varphi }_1,\dots ,{\varphi }_t$, and choose a fixed window length $r$ sufficient to include every sort used and its auxiliary predecessor. Color every increasing $r$-tuple of natural numbers by the vector of truth values of these unraised sentences in its finite rank-window interpretation. There are only $2^t$ colors. The Ramsey's theorem gives an infinite homogeneous set. Choose $r+1$ successive points from it. The first $r$ points and last $r$ points have the same color, while the latter interpretation of ${\varphi }_j$ is exactly the former model's interpretation of ${\varphi }_j^{+}$. The auxiliary predecessor shifts too, so this remains true for sentences mentioning the lowest set predicate. Extend the chosen rank sequence arbitrarily to interpret the remaining sorts. This yields a model of typed set theory satisfying all the specified ambiguity instances.

Thus every finite subset of the typed axioms together with all ambiguity instances has a model. Applying multisorted compactness theorem givesThe final model satisfies first-order typed comprehension, with quantification over its own sorts and sets as in Henkin semantics.

Let $M^{\ast }$ be a full Skolem expansion of an infinite structure $M$, choose distinct $b_n\in M$ for $n\in \mathbb{N}$, and extend the cofinite filter to a nonprincipal ultrafilter $U$ on $\mathbb{N}$. For a finite subset $F=\{i_1<\cdots <i_r\}$ of the desired index order $I$, define the ordered Fubini product of ultrafilters $U_F$ on ${\mathbb{N}}^F$ bywhere $UnP(n)$ means $\{n:P(n)\}\in U$. These nested tests decide complements and preserve intersections by induction on $r$, so $U_F$ is indeed an ultrafilter. For the empty set use the one-point index set and its principal ultrafilter.

Put $M_F=(M^{\ast }{)}^{{\mathbb{N}}^F}/U_F$. If $F\subseteq G$, projection of coordinates inducesA truth test independent of a coordinate is unchanged by its dummy ultrafilter quantifier. Consequently pullback preserves exactly the $U_F$-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 $N^{\ast }$. 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 $a_i$ be the image in this limit of the coordinate class $[n\mapsto b_n]\in M_{\{i\}}$. These elements are distinct: in $U_{\{i,j\}}$, equality would require $n_i=n_j$, whose inner-coordinate section is a singleton and hence not in the nonprincipal $U$. For $i_1<\cdots <i_r$, the truth of any expanded-language formula on $(a_{i_1},\dots ,a_{i_r})$ is exactlyThis expression depends on the formula and the tuple length, not on the chosen increasing indices. Thus $(a_i{)}_{i\in I}$ is an order-indiscernible sequence. The empty-coordinate stage embeds $M^{\ast }$ elementarily into $N^{\ast }$.

Their Skolem hull is elementary by the witness-function argument, and an order automorphism of $I$ 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 $M$ and every total order $I$, an elementary extension contains distinct elements $(a_i{)}_{i\in I}$ forming an order-indiscernible sequence. After a suitable Skolem expansion, their Skolem hull is a first-order model of $\mathrm{Th}(M)$, and every order automorphism of $I$ extends to a structure automorphism of that hull. If $M$ has a definable infinite linearly ordered subset $P$, the generators may lie in $P$ 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 $M$ to $M^{+}$ 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 $\mathcal{U}$ on $\mathbb{N}$.

We can obtain an infinite sequence of distinct elements $b_0,b_1,\dots$ in an elementary extension $M_0$ of $M^{+}$ by one preliminary ultrapower. For each $n\ge 1$ choose a finite list of $n$ distinct elements of $M^{+}$. Represent $b_j$ by the function taking the $j$th entry when $n>j$, 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 $P$, and choose each finite list increasingly inside $P$ instead; then $M_0\models P(b_j)$ and $b_j<b_k$ for $j<k$. Infinitude of an ordered set supplies every finite increasing chain. This preparatory step uses no Ramsey theorem.

For a finite subset $F=\{i_1<\cdots <i_r\}$ of $I$, define the ultrafilter ${\mathcal{U}}_F$ on ${\mathbb{N}}^F$ by nested membership, in this order:where $(\mathcal{U}n)Q(n)$ means $\{n:Q(n)\}\in \mathcal{U}$. 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 $F=\varnothing$ take the principal ultrafilter on the one-point product. PutIf $F\subseteq G$, pull a function back along the projection ${\mathbb{N}}^G\to {\mathbb{N}}^F$. A test independent of an omitted coordinate is unchanged by its ultrafilter quantifier, so projection pushes ${\mathcal{U}}_G$ to ${\mathcal{U}}_F$. The induced map $N_F\to N_G$ is therefore an elementary embedding by Łoś theorem. These maps are coherent, giving a directed system indexed by finite subsets of $I$.

Take its directed limit of elementary embeddings $N$. 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 $N_F$ embeds elementarily into $N$, which contains an elementary copy of $M^{+}$.

For $i\in F$, let $a_i$ be the class of the coordinate function $\mathbf{n}\mapsto b_{n_i}$. Projection coherence makes this independent of $F$. If $i<j$, then for each fixed $n_i$ the set $\{n_j:n_j\ne n_i\}$ is cofinite. The nested test therefore gives $a_i\ne a_j$. In the ordered variant, the same argument with $n_j>n_i$ gives $P(a_i)$ and $a_i<a_j$.

For every first-order formula $\phi$ of the expanded language and every increasing tuple $i_1<\cdots <i_r$, Łoś theorem givesThe 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 $H$ be the Skolem hull of the generators in $N$. The Tarski-Vaught test gives $H\prec N$, and its reduct is a first-order model of $\mathrm{Th}(M)$.

An order automorphism $\pi$ of $I$ acts byIndiscernibility 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 ${\pi }^{-1}$. Every element of the hull is such a term, so the extension is unique among structure automorphisms preserving the Skolem expansion. MoreoverThis proves the theorem, including its ordered version and structure automorphism conclusion, using ultrapowers and a directed limit throughout.

The Ehrenfeucht-Mostowski theorem says that if a first-order theory $T$ has an infinite model, then for every total order $I$ there is a model $M\models T$ generated as the Skolem hull of distinct order indiscernibles $(a_i{)}_{i\in I}$, and every order automorphism of $I$ extends to an automorphism of $M$.

Given an infinite cardinal $\kappa$, let $I=\kappa \times \mathbb{Q}$ with the lexicographic order, viewed as $\kappa$ consecutive copies of the rational order. In each copy independently choose either the identity or a fixed nonidentity order automorphism of $\mathbb{Q}$. These choices give $2^{\kappa }$ distinct order automorphisms of $I$.

Apply the theorem to this order. Distinct order automorphisms act differently on the distinct generators $a_i$, so their extensions give an injection into the automorphism group of a first-order structure $\mathrm{Aut}(M)$. Therefore $|\mathrm{Aut}(M)|\ge 2^{\kappa }$, proving that $T$ has models with arbitrarily large automorphism groups.

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.