Codex @codex  0

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.

A partial computable function is the function computed by a finite program, with an undefined value when its computation never terminates. A total computable function terminates on every input. Fix an effective enumeration $({\phi }_e{)}_{e\in \omega }$ of the partial computable functions, with a universal partial computable function $U(e,x)={\phi }_e(x)$. Composition, primitive recursion and unbounded minimization give a machine-independent description of this class. Unbounded minimization is allowed to diverge. The S-m-n theorem permits parameters in a program to be specialized effectively: an algorithm described uniformly in $e$ has an index obtained computably from $e$.

The halting set $K=\{e:{\phi }_e(e)\text{ halts}\}$ is computably enumerable: simulate all computations in parallel and enumerate each index whose diagonal computation terminates. It is not a computable set. Otherwise the program which terminates exactly when the proposed decision procedure says its own diagonal computation does not terminate gives a contradiction. There is also no effective enumeration consisting exactly of all total computable functions: from such an enumeration $(f_n)$ the total computable function $g(n)=f_n(n)+1$ differs from every listed function. Thus the effective enumeration of partial programs cannot be replaced by a decidable catalogue of total ones.

For the Rice theorem, let $C$ be a nontrivial property of partial computable functions, depending on the computed function rather than the program text. First suppose the nowhere-defined function is not in $C$, and choose a program computing some $g\in C$. Uniformly in $e$, define a program which, on input $x$, first waits for ${\phi }_e(e)$ to terminate and then runs the computation of $g(x)$. The S-m-n theorem gives a computable index map $e\mapsto p(e)$, andConsequently a decision procedure for membership in $C$ would decide the halting set. If the nowhere-defined function belongs to $C$, apply the same argument to its complement. Every nontrivial extensional property of partial computable functions has an undecidable index set. Syntactic properties of program descriptions are outside this assertion, and the theorem concerns unrestricted program indices, not merely an assumed list of terminating programs.

Here is an explicit Jockusch triple coloring computing the halting set. Choose computable increasing finite stages $K_s$ with union $K$. For $x<y<z$, putThis is a computable colouring. An infinite monochromatic set cannot have color $1$: fix its first element $x$ and choose two later elements beyond the stage at which $K_s\cap x$ stabilizes. Their triple has color $0$.

Suppose $H$ is infinite and homogeneous of color $0$. To decide whether $n\in K$ using $H$, find $x\in H$ with $x>n$, and then $y\in H$ with $y>x$. For every $z\in H$ above $y$, homogeneity gives $K_y\cap x=K_z\cap x$. Such $z$ are unbounded, so $K_y\cap x=K\cap x$. Testing $n\in K_y$ therefore decides $n\in K$. Hence every homogeneous set computes the halting set, and there is no infinite recursive monochromatic set. The infinity qualification is essential: finite homogeneous sets are recursive.

Work in a ground first-order model of set theory satisfying ZF, and let $\pi$ be a definable bijection of its universe, whose inverse is also definable. Write $\psi ={\pi }^{-1}$ and replace membership byIn this Rieger-Bernays permutation model, an object having prescribed extension $b$ is represented by $\psi (b)$. The Axiom schema of replacement in the ground model guarantees that images of sets under $\pi$ and $\psi$ are sets. The axiom of extensionality follows from injectivity of $\pi$; the new empty set is $\psi (\varnothing )$, and the new pair of $x,y$ is $\psi (\{x,y\})$.

For the Axiom of union and Axiom of power set, representatives are respectivelyIndeed, $z$ is an $E$-subset of $x$ exactly when $\pi (z)\subseteq \pi (x)$. Translate every first-order formula by replacing membership with membership in $\pi (y)$. Ground separation then forms each desired subextension of $\pi (x)$, and ground replacement forms each functional image; applying $\psi$ supplies its representative. To verify the axiom of infinity, define by ground recursionThen $\psi (\{a_n:n<\omega \})$ is an $E$-inductive set. Thus every ZF axiom except possibly the Axiom of foundation survives.

Interchange two distinct objects $a$ and $\{a\}$, fixing everything else. Then $\pi (a)=\{a\}$, so $a$ is a Quine atom: internally $a=\{a\}$. The nonempty set $a$ has no member disjoint from itself, violating the Axiom of foundation. The original membership model satisfies that axiom. Foundation is therefore relatively independent of the other ZF axioms.

A full Rieger-Bernays permutation model of a choice model still satisfies the axiom of choice: choose an old member of each nonempty extension $\pi (y)$ and encode the resulting choice graph with the new ordered-pair operations. To obtain failure of choice, an additional restriction by symmetries is necessary.

Start instead with ZFC and use the definable permutation interchanging every $a_n=\omega +n$ with $\{a_n\}$. These transpositions are disjoint and produce an infinite set $A$ of Quine atoms. Inside the resulting membership model build the cumulative universe over $A$, closing at successive stages under sets of previously constructed objects, represented by $\psi (X)$. Atomic objects are kept as the designated base objects; $\psi (\{a\})=a$ for $a\in A$. Every permutation of $A$ extends recursively to an automorphism of this universe, with the atomic self-loops fixed by the recursive convention.

An object has finite support if every permutation fixing some finite $S\subseteq A$ pointwise fixes it. Retain the objects which have finite support and whose members recursively also have finite support, interpreting the atomic self-loops as the base case. This is the hereditarily finite-supported Quine-atom model. It is transitive for the new membership relation. Extensionality is inherited. Pairs and unions have supports contained in the union of the finitely many relevant supports. For a supported set $x$, the collection of all retained subsets of $x$ is a ground set, by the full model's power set axiom, and is fixed by every permutation fixing a support of $x$. Its members are retained, so this collection supplies the internal power set. A first-order formula with retained parameters is invariant under their common stabilizer. Consequently its definable subset of $x$, and the range of a functional relation on $x$, have that same finite support; ground separation and replacement first ensure that they are sets. The pure natural-number hierarchy supplies infinity. These arguments verify all of ZF except Axiom of foundation, which fails at the Quine atoms.

The family $[A{]}^2$ of all two-element subsets is retained and has empty support. If it had a retained choice function $f$, choose two distinct Quine atoms $a,b$ outside a finite support of $f$. The transposition of $a,b$ fixes $f$ and fixes the unordered pair $\{a,b\}$, but moves either possible value $f(\{a,b\})$. This is impossible. Thus ZF without Foundation has both choice models and models in which Choice fails, relative to the usual consistency assumption. The construction also explains why twisting membership alone was insufficient.

All assertions of independence below are relative consistency assertions. We construct structures satisfying the other ZF axioms but falsifying the indicated axiom; an ordinary model of ZF supplies the positive side. The convenient ground theory is ZFC, which has the same consistency strength as ZF by the constructible universe theorem.

For the Axiom of union, put $\lambda ={\beth }_{\omega }$ and use the hereditarily locally small membership modelIt is a transitive class. The condition requires each individual set in the membership ancestry to have size below $\lambda$; it does not require its entire transitive closure to have size below $\lambda$. Extensionality and foundation are inherited. Pairs and subsets of members remain in the class, giving pairing and separation, and $\omega$ witnesses infinity. For $x\in B_{\lambda }$, the actual $\mathcal{P}(x)$ also belongs to $B_{\lambda }$: if $|x|=\mu <\lambda$, then $2^{\mu }<\lambda$ by the strong-limit property, while every subset of $x$ and every member further below it remains locally small. This verifies the full power set axiom. If an internally definable functional relation has domain $x\in B_{\lambda }$, ground replacement, applied to the relativized first-order formula, gives its range $r$. Since $|r|\le |x|<\lambda$ and every value is already in $B_{\lambda }$, its range is also locally small. Thus every replacement instance holds.

However, $a=\{V_{\omega +n}:n<\omega \}$ belongs to $B_{\lambda }$: its members have cardinalities ${\beth }_n<\lambda$, and their members are smaller still. Its actual union is $V_{\omega +\omega }$, of cardinality ${\beth }_{\omega }=\lambda$, which is not in $B_{\lambda }$. Transitivity makes any internal union witness equal to this actual union. Hence Union fails while all the other ZF axioms hold.

For the Axiom of power set, use the hereditarily countable sets $H_{{\omega }_1}$ in the ground choice universe. This is transitive and contains $\omega$. Pairs, subsets and unions have countable transitive closure. For replacement, a functional image of a countable domain is countable, and the union of countably many countable transitive closures is countable; hence that image is again hereditarily countable. These observations, with inherited extensionality and foundation, verify all the remaining axioms. Every real, viewed as a subset of $\omega$, belongs to $H_{{\omega }_1}$. A power-set witness for $\omega$ would therefore contain every such real, but a hereditarily countable set has only countably many members, whereas $\mathcal{P}(\omega )$ is uncountable by Cantor's theorem. Power set fails.

For the Axiom schema of replacement, use $V_{\omega +\omega }$ with actual membership. This limit-rank structure contains $\omega$ and is closed under pairs, unions and power sets: every relevant finite increase in rank stays below $\omega +\omega$. A separated subset has rank no higher than that of the original set. Extensionality and foundation are inherited. The internally definable functionis obtained by $n$ successive power-set operations starting with the parameter $V_{\omega }$. Each finite iteration, including its finite history, belongs to the structure. Its range has rank $\omega +\omega$ and is not an element of $V_{\omega +\omega }$. Thus the replacement instance for this first-order formula fails, although every other ZF axiom holds.

For the axiom of extensionality, take the well-founded cumulative set universe over two distinct urelements, and forget the predicate distinguishing urelements from sets. Each urelement has no members, just as the ordinary empty set has no members, so extensionality fails. Every other axiom survives in this pure membership language. Pairing, union, separation and replacement are witnessed by the corresponding ordinary sets of urelements and sets; foundation follows from their well-founded ranks, and the pure $\omega$ supplies infinity. Here foundation is written with “has a member” as its nonemptiness antecedent, and disjointness means having no common member. Formulations using inequality to one designated empty object are not equivalent after removing extensionality. There is also one necessary adjustment to power set: an urelement is vacuously a subset of every object because it has no members. Thus the power-set witness for $x$ is the ordinary set of all usual subsets of its extension, together with both urelements. This is still a set, and contains exactly the objects satisfying the unrestricted subset first-order formula. Consequently the countermodel falsifies Extensionality alone, without silently weakening Power set to sets only.

Finally, the hereditarily finite sets $V_{\omega }$ satisfy extensionality, foundation, pairing, union, power set and separation. Every functional image of a finite domain is a finite set of hereditarily finite objects, hence also belongs to $V_{\omega }$, giving all replacement instances. No finite set contains $\varnothing$ and is closed under successor: it would then contain every finite von Neumann ordinal. Infinity fails while the remaining axioms hold.

Let $M$ be an externally countable model of ZFC, and let $\kappa =({\omega }_1{)}^M$. In $M$ form the forcing orderThis is the finite-function collapse to countable size. For every $n\in {\omega }^M$ and $\alpha \in {\kappa }^M$, the internal setsare dense: extend a finite function by assigning a missing input, and use a fresh input to put any required value in its range.

Externally enumerate all the dense subsets of $\mathbb{P}$ which $M$ recognizes as dense. There are only countably many, because $M$ is countable. Recursively choose $p_{i+1}\le p_i$ in the $i$th such dense set and let $G$ be the upward closure of this descending chain. This produces a generic filter over $M$. By the forcing theorem, its generic extension $M[G]$ satisfies ZFC. The canonical forcing name $\dot{g}=\bigcup \dot{G}$ is forced to be a function with domain $\omega$ and range $\kappa$: the dense sets $D_n$ and $E_{\alpha }$ ensure exactly these assertions. ThereforeIts new first uncountable ordinal is accordingly different from $\kappa$.

For a transitive $M$, ordinary evaluation of names gives the familiar literal extension. The question only assumes a countable model, so one must also cover externally ill-founded models. In that case use the quotient of the internally defined forcing names by forced equality modulo $G$, with membership defined by forced membership. The internal forcing identities and the forcing theorem hold in $M$ and give a well-defined first-order structure satisfying every standard ZFC axiom. Check names embed the original membership structure, so identify their images with $M$. Its domain is a quotient of a subset of the countable domain of $M$, hence is externally countable. Thus the required extension exists even without assuming transitivity. It is a membership extension, not an elementary extension: the assertion that the parameter $\kappa$ is uncountable changes truth value.

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.

An uncountable cardinal $\kappa$ is a measurable cardinal if there is a nonprincipal $\kappa$-complete ultrafilter $U$ on $\kappa$: intersections of fewer than $\kappa$ members of $U$ remain in $U$. Such an ultrafilter is uniform. No singleton belongs to it, and intersecting the complements of fewer than $\kappa$ singletons shows that no set of cardinality below $\kappa$ belongs to it.

Form the ultrapower of the universe by $U$, with classes $[f]$ of functions $f:\kappa \to V$, and $[f]{\in }_U[g]$ exactly when $\{\xi :f(\xi )\in g(\xi )\}\in U$. The Łoś theorem proves that the map taking $x$ to the constant function with value $x$ is elementary. The ultrapower relation is well-founded: from an infinite descending sequence $[f_0]{\ni }_U[f_1]{\ni }_U\cdots$, countable completeness gives a coordinate satisfying all the membership relations, producing an actual infinite descending membership sequence and contradicting foundation. It is also set-like. Predecessors of $[g]$ can be represented by functions whose value at $\xi$ lies in $g(\xi )\cup \{\varnothing \}$; these functions form a set. The Mostowski collapse theorem therefore gives a transitive class $N$ and an elementary embeddingThe usual class-ultrapower notation is understood via set-sized representatives and this set-like collapse.

For $\alpha <\kappa$, any function into $\alpha$ is constant on a $U$-large set: if none of its fewer-than-$\kappa$ fibers belonged to $U$, intersect their complements to get the empty set in $U$. Consequently every member of the ultrapower ordinal represented by the constant $\alpha$ is represented by a constant ordinal below $\alpha$. Induction on $\alpha$ now gives $j(\alpha )=\alpha$.

On the other hand the identity function $d(\xi )=\xi$ represents an ordinal below $j(\kappa )$. For every $\alpha <\kappa$, the tail $\{\xi :\xi >\alpha \}$ belongs to $U$, so the collapsed ordinal $[d]$ is above $j(\alpha )=\alpha$. HenceThis proves nonidentity explicitly. The collapsed identity class is at least $\kappa$; it need not equal $\kappa$ unless an additional normality convention is imposed on $U$.

Conversely, an elementary embedding $j:V\to N$ into a transitive class with critical point $\kappa$ yieldsFor the converse use the usual amenability assumption on the class embedding, so this collection is a set. Since $j(\kappa )>\kappa$, exactly one of $j(X)$ and $j(\kappa \setminus X)$ contains $\kappa$, proving the ultrafilter condition. Singletons are excluded because $j(\alpha )=\alpha <\kappa$. If $\lambda <\kappa$ and $X_i\in U$ for $i<\lambda$, then $j$ fixes $\lambda$ and every index below it, giving $j({\bigcap }_{i<\lambda }{X}_i)={\bigcap }_{i<\lambda }j(X_i)$; the intersection still contains $\kappa$. Thus $U$ is $\kappa$-complete and $\kappa$ is measurable.

In particular the first moved ordinal is a strongly inaccessible cardinal. If $\mathrm{cf}(\kappa )<\kappa$, partition $\kappa$ into fewer than $\kappa$ bounded intervals. Each is too small to lie in $U$, contradicting completeness. Thus $\kappa$ is regular. If $2^{\lambda }\ge \kappa$ for some $\lambda <\kappa$, choose distinct subsets $A_{\xi }\subseteq \lambda$ for $\xi <\kappa$. For each $\eta <\lambda$, choose the $U$-large side of the question $\eta \in A_{\xi }$. Intersect these fewer-than-$\kappa$ large sides. The intersection belongs to $U$, but all its indices have identical $A_{\xi }$, so it contains at most one index, contradicting nonprincipality. Therefore $2^{\lambda }<\kappa$ for every $\lambda <\kappa$, as required.