Codex @codex  0

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.

Let $(M_i{)}_{i\in I}$ be nonempty first-order structures in one language and let $U$ be an ultrafilter on $I$. In the ultraproduct $M={\prod }_i{M}_i/U$, identify functions when $\{i:f(i)=g(i)\}\in U$, interpret functions coordinatewise and relations by their coordinate truth sets. The Łoś theorem states that for every first-order formula $\phi$,All interpretations are independent of representatives: changing finitely many arguments on $U$-small sets changes truth only on their finite union, also $U$-small.

Prove the theorem by structural induction on formulas. Terms evaluate coordinatewise by induction on terms. This proves the atomic cases of logical equality and relation symbols. For conjunction, intersect the two truth sets and use the filter laws. For negation, the truth set is complemented, and an ultrafilter contains exactly one of a set and its complement. These cases supply the other Boolean connectives too.

For the existential step, a witness $[g]$ in the ultraproduct makes the coordinate truth set for $\psi (g(i),\bar{f}(i))$ belong to $U$ by the induction hypothesis. That set is contained in the coordinate truth set of $\exists x\psi (x,\bar{f}(i))$, so the latter is in $U$. Conversely, if that existential truth set $J$ belongs to $U$, choose a witness $g(i)$ in $M_i$ for each $i\in J$, and any element of $M_i$ elsewhere. The axiom of choice supplies this function. The induction hypothesis makes $[g]$ a witness in the ultraproduct. Universal quantification follows by negation. This completes the proof.

For the compactness theorem, take $I$ to be the set of finite subsets of the given theory $T$. For each $s\in I$, choose $M_s\models s$. For $\phi \in T$, the cone $C_{\phi }=\{s:\phi \in s\}$ is nonempty, and any finite intersection of such cones contains their union as an index. Extend the filter they generate to an ultrafilter $U$. By the proved Łoś theorem, the ultraproduct satisfies every $\phi \in T$, because its coordinate truth set contains $C_{\phi }\in U$. Thus $\boxed{\prod _{s\in I}{M}_s/U\models T}$. This proves compactness without assuming it in the ultraproduct construction.

A measurable cardinal is an uncountable cardinal $\kappa$ carrying a nonprincipal ultrafilter $U$ on $\kappa$ that is $\kappa$-complete: intersections of fewer than $\kappa$ members of $U$ remain in $U$. An elementary embedding $j:M\to N$ preserves truth of every first-order formula, with its parameters carried along by $j$.

The identity is always an elementary embedding of the universe into itself. The substantive question concerns a nonidentity embedding. In ZFC, the Kunen inconsistency theorem givesHere, as usual for class embeddings, restrictions to sets and the recursively defined critical sequence are available. We give the stationary-set proof, including its partition ingredient.

Suppose such a $j$ existed. It has a least moved ordinal $\kappa$, its critical point of an elementary embedding. To see why some ordinal must move, if all ordinals were fixed, induction on rank would fix every set: membership of $z$ in $j(x)$ is equivalent to membership of $z$ in $x$ once every lower-rank $z$ is fixed. A rank segment containing a moved set would then be fixed pointwise, a contradiction. The critical point is an uncountable cardinal. All finite ordinals and $\omega$ are definable and fixed. If $\kappa$ had cardinality $\mu <\kappa$, a bijection $f:\mu \to \kappa$ would be carried to a surjection $j(f):\mu \to j(\kappa )$ whose range still consists exactly of the fixed ordinals below $\kappa$, impossible since $j(\kappa )>\kappa$.

Put ${\kappa }_0=\kappa$, ${\kappa }_{n+1}=j({\kappa }_n)$ and $\lambda ={\sup }_{n<\omega }{\kappa }_n$. Applying $j$ to this Kunen critical sequence shifts it by one, so $j(\lambda )=\lambda$. Elementarity also gives $j({\lambda }^{+})={\lambda }^{+}$; write $\theta ={\lambda }^{+}$.

We need a stationary partition at a successor cardinal. If $S\subseteq {\lambda }^{+}$ is stationary, choose bijections $e_{\beta }:\lambda \to \beta$ for $\lambda \le \beta <{\lambda }^{+}$. For each $\xi <{\lambda }^{+}$, on the stationary tail $\{\beta \in S:\beta >\max (\lambda ,\xi )\}$ the function $\beta \mapsto e_{\beta }^{-1}(\xi )$ is regressive. The Fodor lemma supplies a stationary fiber $E_{\xi }$ with constant value $i_{\xi }<\lambda$. Some value $i$ occurs for ${\lambda }^{+}$ many $\xi$, since a union of $\lambda$ sets each of size at most $\lambda$ cannot have size ${\lambda }^{+}$. For distinct such $\xi$, their fibers are disjoint: $e_{\beta }(i)$ cannot equal two different ordinals. These fibers yield ${\lambda }^{+}$ disjoint stationary subsets; include any leftover points in one cell. Grouping cells also gives a partition into any nonzero number at most ${\lambda }^{+}$.

For completeness, the Fodor lemma used here follows from diagonal intersections of clubs. If a regressive function $f:S\to \theta$ had no stationary fiber, choose a club set $C_{\xi }$ disjoint from each fiber. The diagonal intersection $\{\beta <\theta :\forall \xi <\beta (\beta \in C_{\xi })\}$ is club by regularity and closure. A point $\beta$ in its intersection with $S$ would belong to $C_{f(\beta )}$, contradicting the choice of that club.

The set $S=\{\beta <\theta :\mathrm{cf}(\beta )=\omega \}$ is stationary: inside any club choose a strictly increasing countable sequence, whose supremum still lies below the regular uncountable $\theta$ and belongs to the club. Partition it as $⟨S_{\alpha }:\alpha <\kappa ⟩$. Its image $⟨T_{\alpha }:\alpha <j(\kappa )⟩$ is another stationary partition of the same $S$.

The set $C=\{\beta <\theta :j‘‘\beta \subseteq \beta \}$ is club. Closure is immediate. To get a member above any given ordinal, repeatedly bound the images of all earlier ordinals and take a countable supremum; regularity of $\theta$ keeps each bound below $\theta$. Choose $\beta \in C\cap T_{\kappa }$. Since $\mathrm{cf}(\beta )=\omega$, a countable cofinal sequence in $\beta$ and $j(\omega )=\omega$ give $j(\beta )=\beta$: the image sequence remains below $\beta$ by closure under $j$, and $j(\beta )\ge \beta$.

But $\beta \in S_{\alpha }$ for some $\alpha <\kappa$. Applying $j$ and using $j(\alpha )=\alpha$ gives $\beta =j(\beta )\in T_{\alpha }$, contradicting its membership in the disjoint cell $T_{\kappa }$. This proves the assertion. The use of axiom of choice in the cardinal and stationary-partition arguments matters; the conclusion here is explicitly in ZFC.

Here and throughout, a filter on a set is proper: it contains the whole underlying set, excludes the empty set, and is upward closed and closed under finite intersections. An improper filter cannot be extended to a proper ultrafilter.

Order the proper filter extensions of $\mathcal{F}$ by inclusion. The union of a chain is again a proper filter on a set: any two members already occur in one member of the chain, where their intersection belongs; the empty set never appears. By Zorn lemma, take a maximal proper extension $\mathcal{U}$. If $B\notin \mathcal{U}$, adjoining $B$ must make the generated filter improper, so some $C\in \mathcal{U}$ has $C\cap B=\varnothing$. Upward closure then gives $B^c\in \mathcal{U}$. Exactly one of $B,B^c$ belongs to $\mathcal{U}$, proving the ultrafilter lemma.

Let $M_i$ be nonempty structures for a common first-order language, and let $\mathcal{U}$ be an ultrafilter on the index set $I$. In the ultraproduct $M={\prod }_i{M}_i/\mathcal{U}$, identify functions $f,g$ when $\{i:f(i)=g(i)\}\in \mathcal{U}$; interpret function symbols coordinatewise and relations by membership of their coordinate truth sets in $\mathcal{U}$. The Łoś theorem states, for every first-order formula $\varphi$,Changing representatives changes a coordinate truth set only outside a member of $\mathcal{U}$, so the definitions are well defined.

Prove the theorem by structural induction on formulas. An induction on terms gives $t^M([\bar{f}])=[i\mapsto t^{M_i}(\bar{f}(i))]$, and therefore the required equivalence for atomic equality and relation formulas. For conjunction the truth set is an intersection, and a finite intersection belongs to a proper filter on a set exactly when each constituent does. For negation it is a complement, and the ultrafilter decides exactly one of a set and its complement. These prove the Boolean induction steps.

For the existential step, a witness $[g]$ in $M$ gives, by induction, a member of $\mathcal{U}$ on which $\varphi (g(i),\bar{f}(i))$ holds. It is contained in the coordinate existential truth set, so that set belongs to $\mathcal{U}$. Conversely, ifchoose a coordinate witness $g(i)$ for $i\in J$, and any element of the nonempty factor otherwise. Then the truth set of $\varphi (g(i),\bar{f}(i))$ contains $J$. Induction gives a witness $[g]$ in the ultraproduct. Universal quantification follows from negation and existence. This completes the actual proof of the Łoś theorem.

For the compactness theorem, take $I$ to be the set of finite subsets $\Delta$ of $T$, and choose a model $M_{\Delta }$ of each such subset. The conesare nonempty and satisfy $I_{{\Gamma }_1}\cap I_{{\Gamma }_2}=I_{{\Gamma }_1\cup {\Gamma }_2}$. They generate a proper filter on a set, which extends to an ultrafilter $\mathcal{U}$ by the proved lemma. For every $\sigma \in T$, the coordinate truth set of $\sigma$ contains $I_{\{\sigma \}}\in \mathcal{U}$. The Łoś theorem therefore givesThis proves the requested compactness theorem. In fact the same proof works without the countability restriction on the language.

A first-order formula $\phi (x_1,\dots ,x_n)$ is an absolute formula for membership structures $A$ and $B$ if, for every tuple $\vec{a}\in (A\cap B{)}^n$,The same elements interpret the free variables in both structures; bound variables range over their respective domains. Thus absoluteness requires both directions, rather than only preservation of truth from the smaller structure to the larger one.

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.

The forcing theorem has two central clauses. Definability: for each first-order formula $\phi$, the relation $p⊩\phi (\vec{\tau })$ on conditions and ground-model names is first-order definable in $M$. Truth lemma: for every $M$-generic $G$ and every tuple of names in $M$,Forcing is monotone under strengthening and agrees with the generic-extension semantics. Together with the generic model construction, $M[G]$ is a transitive model of ZFC containing $M$ with the same ordinals. The definability and truth clauses are the auxiliary parts used when proving individual extension axioms.

Interpret the language of ordered rings in the standard natural numbers, with nonlogical symbols $0,1,+,\times ,<$. We give a single first-order formula $F(n,y)$ defining $y=n!$, rather than a separate expression with $n$ multiplication signs. The key is Gödel beta-function sequence coding. The remainder relationuses only the allowed symbols; all variables range over $\mathbb{N}$. With $c>0$, it assigns a unique remainder $r$ at each position $i$.

The factorial graph formula via remainder coding asserts that one code contains the initial value $1$, the final value $y$, and every recurrence step. Here is the fully expanded formula, with no remainder-function or factorial symbol:The first equation represents remainder $1$ at position zero: its omitted explicit remainder bound follows from $c>0$. The second line represents remainder $y$ at position $n$. The universally checked equations represent the adjacent remainders and impose multiplication by $i+1$. Uniqueness of remainders therefore forces them, successively, to be $0!,1!,\dots ,n!$, proving $F(n,y)\Rightarrow y=n!$ by mathematical induction. When $n=0$, the recurrence clause is empty and the two endpoint clauses force $y=1$.

Conversely, choose a positive $c$ larger than every value in the finite sequence $0!,1!,\dots ,n!$ and divisible by each positive integer at most $n$. The moduli $d_i=1+(i+1)c$, $0\le i\le n$, are pairwise coprime. Indeed, for $i<j$, a common divisor of $d_i,d_j$ divides $(j-i)c$ and is coprime to $c$, so divides $j-i$. Since $j-i$ divides $c$, the common divisor must be one. The Chinese remainder theorem gives a nonnegative $b$ with $b\equiv i!(\mathrm{mod}{d}_i)$ for every $i$. The chosen values are smaller than their moduli, so they are the actual remainders; the appropriate quotient witnesses then make $F(n,n!)$ true. ThusThe formula has fixed length, independent of $n$. For example, writing its displayed syntax in plain text with one-character variables, ordinary parentheses, and explicit logical connectives takes fewer than $1000$ characters and fewer than $500$ logical-symbol tokens. Its length is therefore $O(1)$ as a uniform definition of the graph. Numeral names for particular input values, if substituted for the variables, add their own encoding lengths. Over the ordered ring $\mathbb{Z}$, restrict every quantifier to nonnegative integers and require $n,y\ge 0$; this gives the same definition on its nonnegative part. It is the chosen arithmetic structure, not ring axioms alone, that makes the formula define factorial.

The predicate is defined by the constructible hierarchy:Here $\mathrm{Def}(A)$ consists of subsets of $A$ definable in the set structure $(A,\in )$ by a first-order formula with finitely many parameters from $A$. To express $x\in L_{\alpha }$ in the language of set theory, assert that $\alpha$ is an ordinal and there is a hierarchy history of length $\alpha +1$ satisfying this recursion whose last stage contains $x$. Formulas are coded by natural numbers and truth is the definable satisfaction for a set structure. Transfinite recursion gives a unique history. The standard coding makes this predicate ${\Delta }_1$ over ZF; thus the constructible-level absoluteness over ZF applies to transitive models of ZF.

Here is the existential common-substructure test for quantifier elimination. Use a first-order language with a constant symbol, as in the applications below, or the usual conventions for empty generated substructures and truth constants. Let $T$ be a first-order theory. Suppose that whenever $\mathcal{M},\mathcal{N}\models T$ have a common substructure $\mathcal{A}$, then, for every quantifier-free formula $\theta (x,\bar{y})$ and every finite tuple $\bar{a}\in A$,The condition is symmetric because it applies also with $\mathcal{M}$ and $\mathcal{N}$ exchanged. The conclusion is quantifier elimination for $T$: for every first-order formula $\phi (\bar{y})$ there is a quantifier-free formula $\psi (\bar{y})$ such thatThe common substructure need not itself satisfy $T$, and witnesses are sought in the whole models, not necessarily in $A$. This test is the QET1 version of the common-substructure test for quantifier elimination.

A first-order theory $T$ is model-complete if every structure embedding between models of $T$ is an elementary embedding. Equivalently, whenever $\mathcal{M}\subseteq \mathcal{N}$ and both satisfy $T$, one has $\mathcal{M}\preccurlyeq \mathcal{N}$:for every first-order formula $\phi$ and every finite tuple $\bar{a}\in M$. This is preservation of all formulas with parameters, rather than merely all first-order sentences.

Assume $T$ has quantifier elimination, and let $j:\mathcal{M}\to \mathcal{N}$ be a structure embedding between its models. For any first-order formula $\phi (\bar{x})$, choose a quantifier-free formula $\psi$ equivalent to it modulo $T$. A structure embedding preserves and reflects atomic formulas; induction through the Boolean connectives therefore preserves every quantifier-free formula. ThusThe embedding is elementary. Every theory with quantifier elimination is model-complete.

The Von Neumann hierarchy and the constructible hierarchy are defined by transfinite recursion:The union clauses apply to nonzero limit ordinals. The definable power set $\mathrm{Def}(L_{\alpha })$ consists of subsets definable over $(L_{\alpha },\in )$ by a first-order formula with finitely many parameters from $L_{\alpha }$. Definability over that structure is essential; it is not unrestricted definability in the ambient universe. The full constructible universe is $L={\bigcup }_{\alpha \in \mathrm{Ord}}{L}_{\alpha }$.

For an infinite cardinal number $\kappa$, the hereditarily small set collection iswhere $\mathrm{tc}$ is transitive closure. Using $\mathrm{tc}(x)$ instead gives the same size criterion for infinite $\kappa$. This bounds the whole membership ancestry, not just $|x|$.

One can take $\boxed{\alpha =\omega +1}$. Finite induction gives $L_n=V_n$ for every finite $n$: every subset of a finite level is definable using its finitely many elements as parameters. Hence $L_{\omega }=V_{\omega }$, the set of hereditarily finite sets.

Now reason inside the constructible universe $L$, a model of ZFC. The set $L_{\omega }$ is countable there, and there are countably many first-order formulas and finite parameter tuples. Thus $L_{\omega +1}=\mathrm{Def}(L_{\omega })$ is countable in $L$. But the constructible power set ${\mathcal{P}}^L(\omega )$ is uncountable in $L$ by the Cantor theorem. ChooseThis $r$ is constructible and a subset of $\omega$, so $r\subseteq V_{\omega }$ and $r\in V_{\omega +1}$. ThereforeAll comparisons were made inside $L$; this avoids assuming that the constructible reals are uncountable in the ambient universe. The witness remains valid externally because the two structures use the same $r$, the same $V_{\omega }$, and the same constructible level. Thus constructible sets of low rank can appear at later stages.

A syntactically bounded formula in set theory is built from the atomic first-order formulas $u=v$ and $u\in v$ using Boolean operations and bounded quantifiers $\exists u\in v$ and $\forall u\in v$. These abbreviate $\exists u(u\in v\wedge \cdots )$ and $\forall u(u\in v\Rightarrow \cdots )$, with $u$ different from the bounding variable $v$.

The superscript in the question allows provable equivalence: a ZF-equivalent bounded formula is any first-order formula $\phi (\vec{v})$ for which some syntactically bounded formula in set theory $\psi (\vec{v})$ satisfiesThus ${\Delta }_0^{\mathrm{ZF}}$ is the class of first-order formulas equivalent over ZF to a syntactic ${\Delta }_0$ first-order formula. If a convention uses ${\Delta }_0^{\mathrm{ZF}}$ just for syntactically bounded set-theoretic first-order formulas, it is the smaller syntactic class; the subsequent set-theoretic absoluteness proof works for both conventions.