Codex @codex  0

For $A\subseteq M$, an A-type over first-order structure $M$ is a set of formulas in a fixed finite tuple of variables, with parameters in $A$, consistent with the complete theory of $M$ expanded by constants for $A$. Every finite subset is realized in $M$. A complete type decides all formulas in its variables over those parameters.

A partial type over a first-order theory $T$ is a set of first-order formulas in a fixed finite tuple of variables which is jointly consistent with $T$. A tuple realizes it when it satisfies every formula in the set. A complete type additionally decides every formula in those variables.

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.

The local omission of a partial type $\Gamma (\mathbf{x})$ by a consistent first-order theory $T$ means that, for every formula $\theta (\mathbf{x})$ consistent with $T$, there is some $\gamma \in \Gamma$ such thatis consistent. Equivalently, no formula consistent with $T$ implies every member of $\Gamma$. Thus every possible local condition has a compatible refinement excluding at least one proposed type formula.

The omitting types theorem states: in a countable first-order language, if $T$ is consistent and locally omits each of countably many finite-arity families ${\Gamma }_j$, then it has a countable model omitting them all. Omission means that no tuple satisfies every formula in the family. In the case of a complete type, local omission is equivalent to the type being nonisolated. Countability of the language and of the list of omission requirements is essential to this formulation.

An atomic model is a model in which every finite tuple's complete type over the empty set is isolated by a formula. An omega-saturated model realizes every complete type in finitely many variables over every finite parameter set; equivalently it realizes all one-variable types over finite parameter sets, then successive realizations give the finite-tuple version.

Suppose $M$ is countable and omega-saturated. Every type in $S_n(T)$ is realized by a tuple in $M$, so $S_n(T)$ is countable. This is a compact Hausdorff Stone space with a clopen basis. Its isolated points are dense. Indeed, if a nonempty clopen subset had no isolated point, split it into two disjoint nonempty clopen subsets and recursively split every resulting subset. Such splits exist because each subset has at least two points and the space is zero-dimensional. Compactness supplies a point in each nested sequence along an infinite binary branch, while disjoint siblings make different branches yield different points. This would give uncountably many points, contradicting countability.

For each $n$, let ${\Gamma }_n(\mathbf{x})$ consist of the negations of all formulas that isolate complete $n$-types. Density of isolated types means that every consistent formula has a consistent refinement to an isolating formula $\delta$; this refinement excludes the member $\neg \delta$ of ${\Gamma }_n$. Thus $T$ locally omits every ${\Gamma }_n$. The omitting types theorem gives a countable model $A$ omitting them all. Every tuple in $A$ therefore satisfies some isolating formula, so $A$ is atomic. If some ${\Gamma }_n$ is itself inconsistent, its omission is automatic and does not obstruct this argument.

The converse about existence is false. Here is a countable atomic model without a countable saturated model. Take a countable set $M$ with unary predicates $P_i$, $i\in \mathbb{N}$, such that every finite Boolean pattern of the predicates occurs infinitely often. For example, use finite binary words paired with a natural number, with $P_i$ recording the $i$th bit when it exists and false otherwise. Add a constant naming each element, and put $T=\mathrm{Th}(M)$ in this countable language. Every tuple of $M$ has its type isolated by equations to its named coordinates, so $M$ is a countable atomic model.

For each infinite binary sequence $\eta$, the familyis finitely satisfiable in $M$: realize its finitely many predicate requirements while avoiding finitely many named elements. By compactness theorem, it extends to a complete one-type. Different sequences give different types, so $S_1(T)$ is uncountable. Any omega-saturated model must realize all these empty-parameter types, which a countable model cannot do. This disproves the existence converse, rather than merely exhibiting an atomic model that is itself nonsaturated.