Codex @codex  0

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.

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 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 nonempty first-order structures $(M_i{)}_{i\in I}$ in a common language and an ultrafilter $D$ on $I$, identify product functions byThe ultraproduct ${\prod }_i{M}_i/D$ has these equivalence classes as elements. Functions are interpreted coordinatewise, and a relation holds of classes exactly when its coordinatewise truth set belongs to $D$. Closure under finite intersections makes these interpretations independent of representatives.

The Łoś theorem assertsProve it by induction on first-order formulas. Atomic first-order formulas hold by the definitions and induction on terms. Conjunction uses intersections, and negation uses the fact that an ultrafilter contains exactly one of a set and its complement. For an existential first-order formula, a product witness gives a coordinate witness on a $D$-large set. Conversely, on the $D$-large set where a coordinate witness exists, choose one in each factor, and choose arbitrary values elsewhere. Its class is a product witness by the induction hypothesis. This is the only witness-selection step; the surrounding argument is made in a choice metatheory. The special case with all factors equal is an ultrapower, and constant functions give an elementary embedding.

Here is a direct compactness theorem proof. Suppose every finite subset of a theory $T$ has a model. Index factors by the finite subsets $i\subseteq T$, choosing $M_i\models i$. For finite $F\subseteq T$, the cone $C_F=\{i:F\subseteq i\}$ is nonempty, and $C_F\cap C_H=C_{F\cup H}$. Extend the generated proper filter to an ultrafilter $D$. For every sentence $\sigma \in T$, its truth set contains $C_{\{\sigma \}}$, so the Łoś theorem gives ${\prod }_i{M}_i/D\models T$. Finite satisfiability therefore implies satisfiability, directly from the ultraproduct construction rather than from a syntactic completeness argument.

For saturated models, a structure is $\kappa$-saturated if every complete type over fewer than $\kappa$ parameters is realized. A useful concrete case is countable saturation of a nonprincipal ultraproduct over omega. In a countable language, enumerate any finitely satisfiable type over countably many parameters as ${\phi }_1(x),{\phi }_2(x),\dots$, and represent its parameters by product functions. By the Łoś theorem, the set $A_n$ of coordinates where the first $n$ first-order formulas have a simultaneous witness belongs to the nonprincipal ultrafilter $D$. PutThese are decreasing $D$-large sets. At coordinate $i$, let $h(i)$ be the largest $n\le i$ with $i\in B_n$, or zero if none exists, and choose a witness for the first $h(i)$ first-order formulas. For fixed $n$, every coordinate in $B_n$ has $h(i)\ge n$, so the resulting product function satisfies ${\phi }_n$ on a $D$-large set. Its class realizes the whole type. Thus such an ultraproduct is ${\aleph }_1$-saturated.

There is also an existence construction at every prescribed degree $\kappa$. Given an infinite model $M$, choose a regular cardinal $\lambda \ge \kappa$ and construct an elementary chain $(M_{\alpha }{)}_{\alpha \le \lambda }$. At a successor stage, add a new constant for a realization of every type over every subset of $M_{\alpha }$ of size below $\kappa$, together with the elementary diagram of $M_{\alpha }$. Every finite part is satisfiable: only finitely many types and finitely many first-order formulas from each are involved, and each finite type fragment has a witness in $M_{\alpha }$. Compactness therefore supplies a simultaneous elementary extension. At limits take unions. To justify elementarity of a union, any existential first-order formula with parameters in an earlier stage has a witness in that stage whenever it has one at a later stage, by elementarity; this is the Tarski-Vaught test.

Any fewer-than-$\kappa$ parameters of $M_{\lambda }$ occur together in some $M_{\alpha }$, by regularity of $\lambda$. A type over them which is finitely satisfiable in $M_{\lambda }$ is finitely satisfiable in $M_{\alpha }$, again by elementarity, and was realized in $M_{\alpha +1}$. Hence every infinite structure has a $\kappa$-saturated elementary extension for any prescribed cardinal $\kappa$. No bound on the size of this extension is asserted; full saturation at the model's own cardinality has additional cardinal-arithmetic issues.

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 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.

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 $\theta ={\xi }^{\ast }$, and work with the set structure $V_{\theta }\models \mathrm{ZFC}$. Its ordinal height is an infinite limit: a transitive model of ZFC has no largest ordinal, since it can take the successor of each ordinal it contains. Thus $\mathrm{cf}(\theta )\ge \omega$.

Suppose instead that $\mathrm{cf}(\theta )>\omega$. Enumerate all first-order formulas, and close each finite initial collection under subformulas. Applying Lévy reflection theorem inside $V_{\theta }$, choose a strictly increasing sequence ${\beta }_m<\theta$ such that $V_{{\beta }_m}$ agrees with $V_{\theta }$ on the first $m$ collections. Take $\eta ={\sup }_m{\beta }_m<\theta$. The internal rank levels here are the actual rank levels, because $V_{\theta }$ is a transitive rank model.

If $V_{\theta }\models \exists x\psi (x,\vec{a})$ with $\vec{a}\in V_{\eta }$, choose $m$ large enough to include this formula and all the parameters in $V_{{\beta }_m}$. Reflection supplies a witness in $V_{{\beta }_m}\subseteq V_{\eta }$. The Tarski-Vaught test therefore gives $V_{\eta }\prec V_{\theta }$. In particular $V_{\eta }$ satisfies all of ZFC, contrary to the minimality of $\theta$.

ConsequentlyThe countable enumeration is of formulas, not merely axioms: witness closure is what makes the union a model of the entire theory.

Put $\mathcal{V}=⟨V_{\kappa },\in ,R⟩$. Because $\kappa$ is inaccessible, $|V_{\xi }|<\kappa$ for every $\xi <\kappa$, and $\kappa$ is regular. Choose one witness in $V_{\kappa }$ for every existential formula of this expanded language and every finite parameter tuple for which a witness exists. These are Skolem functions; they can be chosen in the ambient universe even when $R$ is not definable inside $V_{\kappa }$.

For each $\xi <\kappa$, the ranks of all chosen witnesses with parameters from $V_{\xi }$ have supremum below $\kappa$: there are fewer than $\kappa$ such parameters and only countably many formulas. Choose $F(\xi )<\kappa$ strictly above those ranks. The limit closure pointsform a club set. At $\alpha \in C$, every existential assertion in $\mathcal{V}$ with parameters in $V_{\alpha }$ has a witness in $V_{\alpha }$. The Tarski-Vaught test yieldsThus the set $E$ of all such elementary levels is unbounded. It is also closed: the union at a limit of increasing elementary levels is an elementary substructure by the elementary chain theorem, and the union of their ranks is $V_{\alpha }$ with predicate $R\cap V_{\alpha }$. ThereforeThis is club reflection below an inaccessible cardinal.

A definable continuous hierarchy is a definable class function $\alpha \mapsto H_{\alpha }$ on the ordinals, with set-valued levels, such that $H_{\alpha }\subseteq H_{\beta }$ for $\alpha <\beta$ andfor nonzero limit ordinals. Its union is a definable class in set theory $H$. Often the definition additionally requires every level to be a transitive set; the following statement also works without that requirement.

The reflection theorem for definable hierarchies says that for any finite collection $\mathcal{F}$ of first-order formulas, there is a closed unbounded class of ordinals $\alpha$ such that, for every $\phi \in \mathcal{F}$ and every parameter tuple from $H_{\alpha }$,A useful justification is the witness-closure proof. Close $\mathcal{F}$ under subformulas. At each level and for each existential subformula, bound the least level containing a witness for each parameter tuple for which a witness exists in $H$. Axiom schema of replacement bounds these indices. Iterating the finitely many bounds through $\omega$ produces a limit level containing all required witnesses. Induction on the first-order formulas, equivalently the finite-formula version of the Tarski-Vaught test, yields agreement. Continuity gives closedness of the reflecting class, and starting above any prescribed ordinal gives unboundedness. This is finite reflection, not a claim that all first-order formulas reflect simultaneously in an arbitrary hierarchy.

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 Tarski-Vaught test says that $(M,\in )$ is an elementary substructure of $(N,\in )$ if and only if every existential statement true in $N$ with parameters from $M$ has a witness in $M$ that satisfies its matrix in $N$. Explicitly, for every first-order formula $\psi (x,\bar{y})$ and every parameter tuple $\bar{a}\in M^{|\bar{y}|}$, requireThe truth of the matrix in this test is evaluated in the larger structure $N$. Under this criterion, $(M,\in )\prec (N,\in )$ means that all first-order formulas with parameters from $M$ have identical truth values in the two structures.

The Tarski-Vaught test states that a substructure $M\subseteq N$ is an elementary substructure if and only if every formula $\phi (x,\bar{y})$ and tuple $\bar{a}\in M$ satisfyNecessity follows immediately from elementarity. Conversely, assume the witness condition. Induct on formulas to prove that $M\models \psi (\bar{a})$ exactly when $N\models \psi (\bar{a})$ for every $\bar{a}\in M$. Atomic formulas agree because $M$ is a substructure, and Boolean connectives follow by induction. A witness in $M$ is also one in $N$; a witness in $N$ can be replaced by one in $M$ by hypothesis, after which induction applies to the matrix. Universal formulas follow by negation. Thus the witness condition is equivalent to $M\preccurlyeq N$.

Put $B=N\setminus \mathrm{acl}(A)$. We seek a model containing $A$ and omitting every element of $B$. Every finite set of these omission requirements is satisfiable: if a finite $C\subseteq B$ met every model containing $A$, the supplied result would imply $C\cap \mathrm{acl}(A)\ne \varnothing$, a contradiction.

Apply the compactness theorem to the elementary-diagram formulation of these requirements, using the Tarski-Vaught test to axiomatize the selected elementary submodel. It gives a model $M$ containing $A$ and omitting all of $B$. Part (a) gives $\mathrm{acl}(A)\subseteq M\cap N$, while omission of $B=N\setminus \mathrm{acl}(A)$ gives the reverse inclusion. Therefore

A finite collection of first-order formulas has a closed unbounded class of ordinals whose levels in a definable continuous hierarchy agree with its union for all parameters in the level. Close the collection under subformulas, bound the least witness levels for existential instances on each set-sized stage by Axiom schema of replacement, and iterate these bounds countably. Continuity supplies the closed stages, and induction on formulas proves agreement. The Tarski-Vaught test describes the same witness criterion. For a hierarchy of length an uncountable regular cardinal, bounds stay below that cardinal when every stage has smaller cardinality.

A Skolem expansion adjoins a Skolem function for every existential first-order formula. Iterating through the successively enlarged languages, and taking their union, gives a language with witness functions even for first-order formulas involving previously added functions. Starting from a language of size $\kappa$, the resulting language has size at most $\kappa +{\aleph }_0$. A hull closed under its functions is a Skolem hull and is elementary in the expanded structure by the Tarski-Vaught test.

For each existential first-order formula $\exists y\phi (y,\mathbf{x})$ in a structure, a Skolem function selects a witness when one exists, with an arbitrary default when none exists. An expansion containing these functions satisfiesA subset closed under all such functions is elementary in the original language by the Tarski-Vaught test. Simultaneously choosing these functions is performed in the ordinary classical metatheory with choice.

After choosing a Skolem function for each existential formula, the Skolem hull of $A\subseteq N$ is the smallest subset containing $A$ and closed under those functions. The Tarski-Vaught test makes it an elementary substructure of $N$, and in a countable language an infinite hull has cardinality at most $|A|+{\aleph }_0$.