Codex @codex  0

An inner model of ZF is a transitive class $N$ containing all ordinals and satisfying ZF with the inherited membership relation. The “all ordinals” requirement is important: an arbitrary transitive set model or a rank segment is not an inner model in this sense.

Every such inner model contains the ambient constructible universe $L$. Here is the reason. Inductively $L_{\alpha }^N=L_{\alpha }$. The zero stage is the same empty set. If the stages at $\alpha$ agree, satisfaction for the common set structure $(L_{\alpha },\in )$ is absolute: atomic first-order formulas agree, Boolean operations agree, and quantified variables range over the identical set. The codes of finite first-order formulas are also the same because a transitive model of ZF has the actual natural numbers. Consequently definability with parameters from $L_{\alpha }$ produces exactly the same subsets in both models, so their successor constructible stages agree. At a limit ordinal both constructions take the union of the same earlier stages. This proves agreement at every stage and hence $L\subseteq N$.

The constructible universe theorem provides models of ZF satisfying $V=L$ and the axiom of choice, whenever ZF is consistent. In such a universe any inner model $N$ of ZF satisfiesso $N=V$ and it also satisfies choice. ThereforePassing to $L$ proves the consistency of choice, but the same downward method cannot prove its negation from an arbitrary starting model: it has no possible output when the starting universe is constructible. This is the precise obstruction intended in an inner-model independence argument. It is not a claim that every inner model of every choice universe satisfies choice; symmetric submodels of suitable forcing extensions can fail choice, and that method first changes the ambient universe.

Use the bounded successor characterization of finite ordinals. Let $\mathrm{Ord}(x)$ assert that $x$ is transitive, each of its members is transitive, and any two members are equal or comparable by membership. This is a bounded first-order formula; foundation makes its linear membership order well-founded, so it is precisely the Von Neumann ordinal predicate. Defineand putFor an ordinal, having a greatest member $y$ says exactly $x=y\cup \{y\}$. The displayed definition makes no reference to an infinite inductive set or to $\omega$; all quantifiers are bounded within the candidate and its members. Occurrences of $x=\varnothing$ can also be expressed as $(\forall u\in x)u\ne u$, so no unbounded quantifier is hidden in empty-set notation.

Every usual natural number satisfies this predicate, by induction: it is a finite ordinal, and every nonzero initial segment is a successor. Conversely, suppose an ordinal $x$ is not a usual natural number. Ordinal comparability gives $x\ge \omega$. If $x=\omega$, it has no greatest member, contradicting ${\mathrm{Succ}}_0(x)$. If $x>\omega$, then $\omega \in x$ has no greatest member, contradicting the corresponding bounded requirement on members of $x$. Hence $\mathrm{Nat}(x)$ holds exactly for the usual natural numbers. The axiom of infinity and separation therefore collect this class as the usual set $\omega$. This is a bounded definition of membership in the natural-number class; it does not claim that the infinite set $\omega$ itself can be produced without the infinity axiom.

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.

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.

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.