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 an order-dense subset $D$ of the real line extends uniquely by $\tilde{\phi }(x)=\sup \{\phi (d):d\in D,d<x\}$. Order completeness supplies the extension, and the lower cuts in $D$ give uniqueness.

An ordered group whose partial order is a lattice. Each pair has a join $f\vee g$ and a meet $f\wedge g$. Translations preserve these operations, for example $a(f\vee g)b=afb\vee agb$. Pointwise maximum and minimum make the order automorphisms of a chain into a lattice-ordered group.

A group of order automorphisms of a totally ordered set that is closed under pointwise maximum and minimum. Products act on the right when writing $\alpha f$; then $\alpha (fg)=(\alpha f)g$. The pointwise lattice operations make it a lattice-ordered group.

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.

A useful form of the Ehrenfeucht-Mostowski theorem says that, for an infinite first-order structure $M$ and any total order $I$, there is a model of $\mathrm{Th}(M)$ generated as a Skolem hull by distinct order indiscernibles $(a_i{)}_{i\in I}$. Every order automorphism of $I$ extends uniquely to an automorphism of the specified Skolem expansion of that hull. The model can be obtained inside an elementary extension of a Skolem expansion of $M$; the generated hull itself need not contain $M$.

Choose a Skolem expansion $M^{\ast }$ by iteratively adjoining witness functions: for each existential formula in the current language choose a function returning a witness whenever one exists, with an arbitrary value otherwise. Repeat for countably many rounds. Every formula in the final language uses finitely many symbols, so has a witness function from a later round. Thus the expansion is Skolemized for its own formulas, as required for elementarity of its hull. Add constants $a_i$ for $i\in I$ to the complete theory of $M^{\ast }$, require them to be distinct, and impose the schemefor every formula in the Skolem language. If an elementary extension of $M^{\ast }$ is desired, also add its elementary diagram with separate names for its elements.

Every finite part of this theory is satisfiable. Choose infinitely many distinct elements $b_0,b_1,\dots$ of $M$. For each of the finitely many arities in that fragment, color increasing index tuples by the finite vector of truth values of the formulas occurring. Repeated applications of the infinite Ramsey theorem give an infinite subset on which all these vectors are constant. Interpret the finitely many $a_i$ in increasing-index order from that subset. This satisfies the finite indiscernibility requirements and distinctness, while the elementary diagram is satisfied by the named original structure. The compactness theorem gives a structure $N^{\ast }$ satisfying the whole theory.

Let $H$ be the closure of the $a_i$ under the Skolem functions, including nullary ones. It is elementary in $N^{\ast }$: whenever an existential formula with parameters from $H$ is true in $N^{\ast }$, its Skolem witness lies in $H$. This is the Tarski-Vaught test, whose proof is induction on formulas, using precisely this witness property for the existential step. Hence the reduct of $H$ is a model of $\mathrm{Th}(M)$.

For an order automorphism $\sigma :I\to I$, defineThis is well-defined. If two terms denote the same element, write their equality as a formula on the combined increasing tuple of their indices; indiscernibility preserves that formula after transport by $\sigma$. The same argument preserves every relation and function. Applying ${\sigma }^{-1}$ gives the inverse, so $\hat{\sigma }$ is an automorphism. Since all elements are terms in the generators, it is the unique automorphism of this Skolem expansion extending $a_i\mapsto a_{\sigma (i)}$. This proves the theorem.

One may require the indiscernibles to lie in any specified infinite sequence of the starting structure, or to satisfy additional finite-tuple properties holding along that sequence: the same finite satisfiability proof chooses its homogeneous subsequence there. This strengthened form is what the rank-domain construction of NFU uses. Uniqueness is asserted in the Skolem expansion, not for all automorphisms of its reduct.

For each $g\ne 1$, choose a value in a lattice-ordered group $P_g$, using Zorn's lemma. Such a value is a prime convex lattice subgroup. Otherwise the last construction in Question 1(i) would give two larger convex lattice subgroups whose intersection is $P_g$; maximality among subgroups omitting $g$ would put $g$ in both, hence in their intersection. Thus the right coset set ${\Omega }_g=P_g\backslash G$ is a totally ordered set.

Right multiplication defines an action ${\rho }_g(a):P_{g}h\mapsto P_{g}ha$. It is well-defined, preserves the total order, and has inverse ${\rho }_g(a^{-1})$. The coset formulas from Question 1(i) show pointwise preservation of both join and meet, becauseand likewise for the meet.

Take the disjoint union of these chains, arranged in any fixed order sum of the indices $g\ne 1$. Let every $a\in G$ act on each component by ${\rho }_g(a)$. This gives a lattice-ordered group homomorphism into the order automorphisms of one chain. It is injective: a nonidentity $a$ moves the identity coset in ${\Omega }_a$, since $P_{a}a\ne P_a$. Its image is closed under pointwise join and meet, giving exactly the required lattice-ordered permutation group. This is the Holland representation theorem.

Construct the conjugacy of positive real-line bumps using $u=v=\alpha$. Since both $\alpha f$ and $\alpha g$ are greater than $\beta$, choose the fundamental-interval map to be identity on $[\alpha ,\beta ]$ and then increase from $\beta$ to the respective right endpoints. Equivariant extension along $f$ and $g$ gives a conjugator on their supports fixing $[\alpha ,\beta ]$. Extend it over the remaining portions of $J=[\gamma ,\gamma h]$, fixing the endpoints of $J$; both support intervals lie strictly inside $J$. Call the resulting interval bijection $b_0$. It satisfies $f{b}_0=b_{0}g$ on $J$.

The point $\gamma$ lies in a positive orbital of $h$, because $\gamma h>\gamma$. Its half-open cells $J{h}^n$, $n\in \mathbb{Z}$, partition that orbital. Extend byand set $b$ to identity outside the orbital. Since $b_0$ fixes the cell endpoints, this is an order automorphism and satisfies $bh=hb$. Each cell is preserved; $f$ and $g$ are identity on all cells other than the original one, so $fb=bg$ holds everywhere. Finally $b$ fixes $[\alpha ,\beta ]$ pointwise, and $a$ is supported inside that interval. Hence $ba=ab$. ThusThis is conjugating positive bumps while preserving a fundamental interval; merely choosing an arbitrary conjugator would not ensure either commutation relation.

Write the two supports as $I_f=(l_f,r_f)$ and $I_g=(l_g,r_g)$. Every point in a support moves strictly right: a positive nonidentity order automorphism has no fixed point inside its one support interval. Choose $u\in I_f$, $v\in I_g$ and an increasing bijection $\theta :[u,uf]\to [v,vg]$ matching endpoints. The half-open intervals $[u{f}^n,u{f}^{n+1})$, for $n\in \mathbb{Z}$, partition $I_f$, because the iterates tend to its endpoints. DefineThe endpoint choices make adjacent pieces fit, giving an increasing bijection $b:I_f\to I_g$ with $fb=bg$. Extend over the two complementary closed rays by increasing maps taking $l_f,r_f$ to $l_g,r_g$. Outside the supports both automorphisms are identity, so $fb=bg$ still holds. Therefore $\boxed{b^{-1}fb=g}$. This gives the conjugacy of positive real-line bumps.

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.

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.

We prove the Ehrenfeucht-Mostowski theorem by ordered products of ultrafilters, without using Ramsey's theorem. Choose a Skolem expansion $M^{\ast }$ of the infinite structure and distinct elements $b_0,b_1,\dots$. Fix a nonprincipal ultrafilter $U$ on $\mathbb{N}$.

For a finite increasing 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$ byThe notation $UnP(n)$ means that the set of $n$ satisfying $P$ belongs to $U$; the leftmost quantifier is outermost. Upward closure and intersection follow successively at each coordinate, and applying complement at each step proves the ultrafilter dichotomy. Products are ordered; no false claim of symmetry is needed.

Put $M_F=(M^{\ast }{)}^{{\mathbb{N}}^F}/U_F$, with $M_{\varnothing }=M^{\ast }$. If $F\subseteq G$, pullback of a function by coordinate projection inducesFor a cylinder condition involving only coordinates in $F$, deleting the unused ultrafilter quantifiers makes its membership in $U_G$ exactly its membership in $U_F$. The Łoś theorem therefore makes ${\sigma }_{FG}$ an elementary embedding, not merely a homomorphism. The projection identities give ${\sigma }_{GH}{\sigma }_{FG}={\sigma }_{FH}$.

Take the directed limit of this system: elements from two stages are identified if their images agree at a common larger finite stage, and formulas are evaluated at such a stage. Elementary coherence makes this well-defined. It also makes each stage elementary in the limit: a formula uses finitely many parameters, and an existential witness at a later stage can be pulled back at the level of existential truth because the transition maps are elementary. Denote the limit by $N^{\ast }$.

For each $i\in I$, let $a_i$ be the limit image of the coordinate function $n_i\mapsto b_{n_i}$. These elements are distinct. For $i<j$, after fixing $n_i$, equality $b_{n_i}=b_{n_j}$ holds for at most one $n_j$, a set not in $U$; hence equality fails in the two-coordinate ultrapower and therefore in the limit.

For any increasing $i_1<\cdots <i_r$, Łoś evaluatesThe right-hand side depends on the formula and the number of increasing coordinates, not their particular indices. Thus $(a_i{)}_{i\in I}$ is order-indiscernible for every formula of the expanded language simultaneously; no preliminary homogeneous thinning is used. If elements of $M$ were named before expanding, the same computation gives indiscernibility over those names and the initial stage embeds the original structure into the limit.

The Skolem hull of these generators is elementary by the witness property. Transporting the generators by any order automorphism of $I$ transports every term, with well-definedness and relation preservation supplied by the formula equivalence just proved. The inverse transport supplies an inverse automorphism. The ordered-ultrapower construction gives the full Ehrenfeucht–Mostowski model and its order automorphisms without Ramsey's theorem.

Write $\mathfrak{c}=2^{{\aleph }_0}$ and enumerate all nonidentity order automorphisms of the real line as $⟨h_{\alpha }:\alpha <\mathfrak{c}⟩$. We construct sets of points to include and exclude, starting with $I_0=\mathbb{Q}$ and $E_0=\varnothing$.

At stage $\alpha$, each of $I_{\alpha },E_{\alpha }$ has cardinality less than $\mathfrak{c}$. Since $h_{\alpha }$ is a nonidentity increasing bijection, its moved points contain a nonempty open interval. Indeed if $h_{\alpha }(u)>u$, points between $u$ and $h_{\alpha }(u)$ are moved; the other direction is similar. There are therefore $\mathfrak{c}$ moved points. Choose one, $x_{\alpha }$, outsideThen put $x_{\alpha }$ into $I$ and $h_{\alpha }(x_{\alpha })$ into $E$. They are different, and the included and excluded sets remain disjoint. Take unions at limit stages. This recursion works even when $\mathfrak{c}$ is singular: before stage $\alpha$, only countably many initial points and at most $|\alpha |$ chosen pairs have been used.

Let $X=\mathbb{Q}\cup \{x_{\alpha }:\alpha <\mathfrak{c}\}$. It is an order-dense subset of cardinality $\mathfrak{c}$. Any nonidentity order automorphism of $X$ extends uniquely to some $h_{\alpha }$ of $\mathbb{R}$, but its value at $x_{\alpha }\in X$ is the excluded point $h_{\alpha }(x_{\alpha })\notin X$, a contradiction. Thus the resulting rigid dense subset of the real line satisfies

If two order automorphisms agree on $\mathbb{Q}$, their values at any real $x$ are the same supremum of the common values at rational points below $x$. This is the uniqueness argument for extension of an order automorphism from a dense subset; it does not require either automorphism to carry $\mathbb{Q}$ onto itself.

Their restrictions belong to ${\mathbb{R}}^{\mathbb{Q}}$, whose cardinality isThis gives the upper bound. The translations $x\mapsto x+r$, one for each real $r$, are distinct order automorphisms, giving the lower bound. Consequently

Use the order completeness of $\mathbb{R}$ to defineThe set in this supremum is nonempty and bounded above: choose $d_0,d_1\in D$ with $d_0<x<d_1$, using that $D$ is an order-dense subset. For $x\in D$, all its displayed values lie below $\phi (x)$. If $y<\phi (x)$, choose $e\in D$ with $y<e<\phi (x)$; then $d={\phi }^{-1}(e)<x$. Thus the supremum equals $\phi (x)$.

The extension is strictly increasing. If $x<y$, choose $d,e\in D$ with $x<d<e<y$; thenApply the same construction to ${\phi }^{-1}$, obtaining $\psi$. For $d<x$, choose $e\in D$ with $d<e<x$; this gives $\phi (d)<\tilde{\phi }(x)$. For $d>x$, a point of $D$ between $x$ and $d$ similarly gives $\phi (d)>\tilde{\phi }(x)$. HenceTaking inverse images and a supremum shows $\psi (\tilde{\phi }(x))=x$. The symmetric argument gives $\tilde{\phi }(\psi (y))=y$, so the extension is an order automorphism.

For uniqueness, any increasing extension $h$ has the same strict lower cut in $D$ at its value $h(x)$. Two distinct real numbers have different cuts in an order-dense subset, so $h(x)=\tilde{\phi }(x)$. The extension exists and is unique.

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.

A positive bump of the real line is an order automorphism whose nonempty support of a permutation is one open interval and which moves every point of that interval to the right. It fixes the complement. Iterating any interior point tends to the right endpoint in positive time and to the left endpoint in negative time.