Codex @codex  0

The saturated model condition in degree $\kappa$ means that a first-order model $M$ realizes every one-variable complete type over a parameter set $A\subseteq M$ of size less than $\kappa$. Equivalently every finitely satisfiable such complete type is realized, since it can be extended to a complete type. Without a specified degree, saturated usually means $|M|$-saturated. Countable saturation means ${\aleph }_1$-saturation, including complete types over countably many parameters.

Here is a general saturated elementary extension theorem, with proof: for every infinite regular cardinal $\kappa$, every first-order structure $M$ has a $\kappa$-saturated elementary extension. At a stage $M_{\alpha }$, list all complete types over its subsets of size less than $\kappa$. There is a set of them, since their formulas lie in a set-sized language. Add a witness constant for each complete type to the elementary diagram of $M_{\alpha }$, together with every formula in that complete type evaluated at its witness constant. A finite part mentions finitely many complete types and finitely many formulas from each; each finite conjunction is realizable in $M_{\alpha }$, and the witnesses for different complete types are unconstrained relative to each other. Thus the finite part is satisfiable. The compactness theorem produces an elementary extension $M_{\alpha +1}$ realizing all those complete types. At limits take elementary unions, justified by the elementary chain theorem.

Iterate for $\kappa$ stages and put $N={\bigcup }_{\alpha <\kappa }{M}_{\alpha }$. If $A\subseteq N$ has size below $\kappa$, regularity bounds the stages at which its elements enter, so $A\subseteq M_{\alpha }$ for some $\alpha <\kappa$. A complete type over $A$ consistent with $N$ is finitely satisfiable in $M_{\alpha }$: each finite conjunction is an existential formula with parameters from $M_{\alpha }$, and elementarity transfers its truth from $N$. The complete type is therefore realized in $M_{\alpha +1}$. This provesFor a singular desired degree, apply the theorem at a larger regular cardinal. If $M$ is infinite and an uncountable regular $\kappa$ satisfies ${\kappa }^{<\kappa }=\kappa$, with $|L|<\kappa$ and $|M|\le \kappa$, the construction can keep every stage of size $\kappa$. There are then at most $\kappa$ parameter sets and complete types, and downward Löwenheim-Skolem gives that size after each extension; adding $\kappa$ distinct elements initially ensures final size exactly $\kappa$. The resulting model is saturated in the unqualified sense. The cardinal-arithmetic hypothesis belongs to this size refinement, not to the general existence theorem.

An explicit ultraproduct version is useful too. In a countable language let $U$ be a nonprincipal ultrafilter on $\omega$ and $N={\prod }_{i<\omega }{M}_i/U$, where each factor is nonempty. Enumerate a countable finitely satisfiable complete type, including its chosen parameter representatives, as ${\phi }_1(x),{\phi }_2(x),\dots$. By the Łoś theorem, the set $A_n$ of coordinates where the first $n$ formulas have a simultaneous witness belongs to $U$. PutThese are decreasing members of $U$. At coordinate $i$, let $k(i)$ be the greatest $n\le i$ with $i\in B_n$, if there is one. Choose a witness to the first $k(i)$ formulas there, and an arbitrary element when there is none. For fixed $n$, every coordinate in $B_n$ has $k(i)\ge n$, so the chosen function satisfies ${\phi }_n$ on a $U$-large set. Its ultraproduct class realizes the whole complete type. A countable language over a countable parameter set has only countably many formulas, so this proves countable saturation of a nonprincipal ultraproduct over omega.

For NFU, we give the rank-indiscernible construction of an NFU model explicitly. NFU has a unary predicate $S$ for sets, atoms have no members, extensionality applies to sets, and comprehension applies to every stratified formula. A stratification assigns integer types to variables so that equality uses equal types and $x\in y$ requires $\mathrm{type}(y)=\mathrm{type}(x)+1$. A unary set predicate adds no type difference.

Start with the actual set structure $B=(V_{\omega +\omega },\in )$. This structure satisfies extensionality and every pure-membership separation instance: the subset defined in a set $a$ of rank below $\omega +\omega$ still has rank below $\omega +\omega$. We do not assert that $B$ satisfies replacement or all of ZFC. Expand it by Skolem functions. In it use the sequence of rank objects $V_{\omega +n+6}$, $n<\omega$. For two such objects $d<e$ in sequence order, we havewith quantifiers in $B$. The second statement holds because every subset of $V_{\alpha }$ belongs to $V_{\alpha +1}$, and the later rank is at least $\alpha +1$.

Introduce constants $d_i$, $i\in \mathbb{Z}$, and require them to be order indiscernibles in the Skolem language, satisfying these two assertions whenever $i<j$. Also require $V_{\omega +5}\subseteq d_i$ for every $i$; this fixed rank object is first-order definable in $B$. Every finite part of these requirements together with $\mathrm{Th}(B^{\ast })$ is satisfiable: color finite increasing tuples of the original rank sequence by the truth values of the finitely many formulas mentioned, and use Ramsey's theorem to get a homogeneous subsequence. The rank assertions hold for every increasing tuple there. The compactness theorem gives a model of the full theory. In its Skolem hull $N$ generated by the $d_i$, the integer shift extends to an automorphism $j$ with $j(d_i)=d_{i+1}$, by the term-transport proof of the Ehrenfeucht-Mostowski theorem. Thus $N$ still satisfies extensionality and all pure-membership separation instances, andThis is a set-sized first-order model; no satisfaction predicate for a proper-class universe is being assumed.

Externally let $D_i=\{x\in N:N\models x\in d_i\}$. The automorphism bijects $D_i$ onto $D_{i+1}$. Interpret a typed structure with sort $i$ equal to $D_i$. At sort $i+1$, declare $y$ a set exactly when $N\models y\subseteq d_i$; otherwise it is an atom. Define adjacent-sort membership byThe guard is necessary: a typed atom might have some ordinary $N$-members in $D_i$, and those must not become its typed members. Set-extensionality follows from extensionality in $N$, because the ordinary members of a typed set all lie in $D_i$. For any typed formula on sort $i$, its quantifiers can be restricted to the corresponding $d_l$, its set predicates replaced by subset assertions, and its memberships replaced by the guarded relation. This is an ordinary pure-membership formula of $N$ with finitely many parameters. Separation gives its extension $X\subseteq d_i$, and the displayed closure assertion gives $X\in d_{i+1}$. It is therefore a typed set witnessing comprehension. The automorphism shifts these sorted domains and preserves the set flags and guarded memberships.

Collapse the types onto $D_0$. DefineObjects not satisfying $S$ have no $E$-members. If two sets have the same $E$-members, their images under $j$ are subsets of $d_0$ with the same ordinary members, so are equal by extensionality of $N$; injectivity of $j$ gives equality of the original objects.

To verify every stratified comprehension instance, assign a variable $v$ its stratification type $t(v)$ and translate its value $a\in D_0$ to $j^{t(v)}(a)\in D_{t(v)}$. Equality is preserved. An atomic $E(x,y)$ translates to the guarded adjacent-sort membership because $t(y)=t(x)+1$; the unary predicate $S(y)$ translates to $j^{t(y)}(y)\subseteq d_{t(y)-1}$. Induction on formulas, using the domain bijections for quantifiers, preserves truth. If the free variable $x$ has type $t$, typed comprehension produces its extension $X\subseteq d_t$, with $X\in d_{t+1}$. Put $b=j^{-(t+1)}(X)\in D_0$. Then $S(b)$ holds, and for every $a\in D_0$,This is exactly the required NFU set. No formula containing the external automorphism $j$ has been used in a separation or comprehension scheme; $j$ only transports values after the pure formula is formed.

The construction also permits the usual infinity requirement. The ordinary $\omega$ and its successor graph $f$ are definable in $N$, hence fixed by $j$, and lie below $V_{\omega +5}$, so belong to all the required domains. Under $E$, the members of $\omega$ are still its ordinary $N$-members. The new Kuratowski pair satisfiesSince $j(f)=f$, membership of this pair in $f$ under $E$ is equivalent to $⟨x,y{⟩}_N\in f$. Thus $f$ is an internal injection of $\omega$ into itself omitting zero, giving a Dedekind-infinite set.

We have built a model of NFU, with infinity if it is included in the formulation, in ordinary ZFC metatheory:In particular $\mathrm{Con}(\mathrm{ZFC})\Rightarrow \mathrm{Con}(\mathrm{NFU})$. This proof does not assume $\mathrm{Con}(\mathrm{ZFC})$ as an additional internal axiom: its starting structure is the set $V_{\omega +\omega }$, not a model of ZFC.

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.