Codex @codex  0

A Henkin construction enlarges a consistent first-order theory by fresh constants, decides sentences while preserving consistency, and supplies constant witnesses for existential sentences. Countably many additional dense requirements can be interleaved, as in the omitting types theorem. A complete consistent extension with witnesses has a term model.

A first-order theory locally omits a family $\Gamma (\mathbf{x})$ if every formula $\theta (\mathbf{x})$ consistent with it has a consistent refinement $\theta \wedge \neg \gamma$ for some $\gamma \in \Gamma$. Equivalently no consistent formula implies all of $\Gamma$. In a countable language the omitting types theorem converts this local condition into a countable model with no realization of the family.

A nonprincipal complete type has no first-order consistent first-order formula implying all its members. In a complete countable first-order theory such a partial type can be omitted in a countable first-order model by the omitting types theorem. A partial type realized by a parameter-free definable tuple is principal.

A partial type is nonprincipal when it is not a principal partial type. Equivalently, for every formula $\theta (\mathbf{x})$ consistent with $T$, some $\psi \in p$ makes $\theta \wedge \neg \psi$ consistent with $T$. This is the exact extension property needed in the Henkin construction proving the omitting types theorem.

In a model of Peano arithmetic, an element realizes this partial type exactly when it is not a standard numeral. A model omitting it is isomorphic to the standard natural-number structure. For a complete consistent extension $T$ of arithmetic, the type is nonprincipal exactly when $T$ is the theory of true arithmetic: apply the omitting types theorem in one direction and use an actual standard witness to refute any proposed isolating formula in the other. For incomplete theories, a principal partial type can still be omitted by some models.

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.

We work with the usual infinite-model convention for an omega-categorical theory: it has a unique countably infinite model up to isomorphism. The three conditions are the type-space and automorphism formulations of the Ryll-Nardzewski theorem; the following arguments prove them rather than invoke that theorem. The standard hypothesis that $T$ has infinite models is understood. If finite models are allowed instead, uniqueness among models of size at most countable is the matching convention for condition (i).

We first prove (i) implies (ii). Suppose some type space $S_n(T)$ were infinite. An infinite compact space cannot have every point isolated: its cover by singleton open sets would have no finite subcover. Thus it has a nonisolated complete type $p$. The omitting types theorem gives a countable model omitting $p$. On the other hand, compactness theorem gives a model realizing $p$, and the Downward Lowenheim-Skolem theorem gives a countable elementary submodel containing its realizing tuple. These countable models cannot be isomorphic, since an isomorphism preserves realization of $p$. This contradicts omega-categoricity. Hence every $S_n(T)$ is finite.

A precise countable-language form of the omitting types theorem is the following. Let $T$ be a consistent first-order theory in a countable first-order language, and let $(p_j({\bar{x}}_j){)}_{j\in \mathbb{N}}$ be a countable family of nonprincipal partial types, each in finitely many variables. Then there is a finite or countably infinite model of $T$ omitting all the $p_j$.

A partial type is a set of formulas jointly consistent with $T$. It is principal if there is a formula $\theta (\bar{x})$ such that $T\cup \{\exists \bar{x}\theta \}$ is consistent andFor a complete type, this is exactly being an isolated type. Nonprincipal means that no such formula exists. A model omits $p$ if no tuple in that model satisfies every formula in $p$; different tuples may fail different members of the type. The model in the theorem need not omit each individual formula everywhere.

For parameter types, use the expanded language naming the parameters. Countability then applies to that expanded language, and hence requires a countable parameter set as well. There is no countability restriction in the finite-satisfiability argument of part (a).

Use the countable-language hypothesis of the omitting types theorem, which is the usual convention for this prime-model result. Let $\mathcal{M}$ be a prime model of $T$ and $a\in M$.

First, $T$ is complete up to logical consequence: every model $\mathcal{N}\models T$ receives an elementary embedding of $\mathcal{M}$, so it satisfies exactly the same sentences as $\mathcal{M}$. We may therefore replace $T$ by $\mathrm{Th}(\mathcal{M})$ without changing its model class or the prime model property.

Suppose $p={\mathrm{tp}}^{\mathcal{M}}(a/\varnothing )$ were not isolated. The omitting types theorem, applied to this single complete type, would produce $\mathcal{N}\models T$ omitting $p$. By primality choose an elementary embedding $j:\mathcal{M}\to \mathcal{N}$. For every $\phi (x)\in p$,Then $j(a)$ realizes $p$, contradicting omission. ConsequentlyThe same proof applies to every finite tuple, giving an atomic model. Countability of the language is a hypothesis of this argument, not a restriction on parameter sets in the separate parts (a) and (d). The PDF does not state that standing hypothesis explicitly; it must be included when invoking this version of the theorem.

The countable form of the omitting types theorem is as follows. Let $L$ be a countable first-order language and $T$ a consistent first-order theory in $L$. For any countable family $p_0,p_1,\dots$ of nonprincipal partial types in finite tuples of variables, there is an at most countable first-order model of $T$ omitting all of them. Nonprincipality means that no $T$-consistent first-order formula $\theta (\mathbf{x})$ entails every member of the type modulo $T$. A complete first-order theory with nonisolated complete types is the usual special case; neither an uncountable language nor an arbitrary uncountable family is covered by this statement.

Use the Godel completeness theorem to pass between consistency and the existence of a first-order model. Adjoin a countable stock $C$ of new constants. Construct finite conditions ${\Gamma }_s$ with $T\cup {\Gamma }_s$ consistent, interleaving three countable lists of requirements: decide each $L(C)$-sentence; provide a fresh constant witness for each existential sentence; and, for each $p_i$ and each tuple $\mathbf{t}$ of closed terms of its arity, add $\neg \psi (\mathbf{t})$ for some $\psi \in p_i$. Sentence decisions preserve consistency by choosing a consistent sign. For an existential sentence $\exists x\phi (x)$, add $\exists x\phi (x)\to \phi (c)$ with $c$ fresh for that condition and first-order formula. This is consistent: any first-order model of the old condition can interpret $c$ as a witness if one exists, and otherwise arbitrarily in the nonempty domain.

The omission step is the key Henkin omission extension lemma. Let $\sigma (\mathbf{c})$ be the logical conjunction of the current finite condition, listing every new constant occurring either there or in $\mathbf{t}$. If adding $\neg \psi (\mathbf{t})$ were inconsistent for every $\psi \in p_i$, then $T$ would entail $\sigma (\mathbf{c})\to \psi (\mathbf{t}(\mathbf{c}))$ for each such $\psi$. Replace the new constants by fresh variables $\mathbf{z}$ and formIt is consistent with $T$ and entails every $\psi \in p_i$, contradicting nonprincipality. Hence some omission extension is consistent. The construction need not be computable; countability merely permits all these requirements to be scheduled.

Let $T^{\ast }$ be the deductive closure of $T\cup {\bigcup }_s{\Gamma }_s$. It is consistent by the finite character of formal proofs, complete by sentence decisions, and has the Henkin witness property. Its term model consists of closed terms modulo provable logical equality and has at most countably many elements. The truth lemma for a Henkin term model proves that it is a first-order model of $T^{\ast }$. Every tuple in it is represented by closed terms, whose scheduled omission requirement supplies a negated member of each corresponding type. Thus

A universal sentence has the form $\forall \mathbf{x}\psi (\mathbf{x})$ with quantifier-free $\psi$, including an empty quantifier block. Embeddings preserve and reflect quantifier-free truth, so universal sentences pass to substructures of a first-order structure. For the converse Łoś-Tarski preservation theorem, let $T_{\forall }$ be all universal consequences of an arbitrary first-order theory $T$, and take $A\models T_{\forall }$. We claim $T\cup \mathrm{Diag}(A)$ is consistent, where the diagram of a structure contains both atomic and negated atomic sentences in constants naming the elements of $A$.

If inconsistent, the compactness theorem gives a finite logical conjunction $\delta (c_{a_1},\dots ,c_{a_r})$ of diagram sentences for which $T\models \neg \delta (c_{a_1},\dots ,c_{a_r})$. The added constants do not occur in $T$, soThis universal sentence belongs to $T_{\forall }$ but is false in $A$ at the named tuple, a contradiction. The compactness theorem therefore produces $B\models T$ containing an isomorphic embedded copy of $A$. The signed diagram ensures a genuine substructure of a first-order structure: functions are preserved, constants are included and relations are preserved and reflected. If the first-order model class of $T$ is closed under substructures of a first-order structure, this copy, and hence $A$, is a first-order model of $T$. We have provedNo countability assumption is needed for this second argument. An inconsistent first-order theory is covered as well, with a universally false axiom and an empty first-order model class.

Use the following form of the omitting types theorem. Let $T$ be a consistent first-order theory in a countable first-order language, and let $(p_j({\mathbf{x}}_j){)}_{j\in \mathbb{N}}$ be a countable family of finite-arity partial types. Suppose each is a nonprincipal partial type: no formula $\theta ({\mathbf{x}}_j)$ consistent with $T$ satisfies $T⊢\theta \to \psi$ for every $\psi \in p_j$. Then $T$ has a countable model omitting all the $p_j$.

For the proof, add countably many fresh constants and perform a Henkin construction. Enumerate three kinds of tasks: deciding each sentence, providing a fresh constant witness for each existential sentence, and making every constant tuple omit each $p_j$ of the corresponding arity. Starting with the empty set, keep a finite set ${\Gamma }_s$ such that $T\cup {\Gamma }_s$ is consistent. A sentence can be decided in one of its two ways while preserving consistency. For an existential sentence, add $\exists x\alpha (x)\to \alpha (c)$ with $c$ fresh; inconsistency would contradict freshness and the existential sentence itself.

For an omission task at a tuple $\mathbf{c}$, let $\gamma$ be the conjunction of ${\Gamma }_s$. Replace its constants by variables, identify the occurrences of the tuple's constants with the corresponding variables $\mathbf{x}$, and existentially quantify the other variables. If the tuple repeats a constant, include the corresponding equalities between its variables. This gives $\theta (\mathbf{x})$ with $T\cup \{\exists \mathbf{x}\theta \}$ consistent. Nonprincipality supplies $\psi \in p_j$ such thatis consistent. Reintroducing the constants shows that ${\Gamma }_s\cup \{\neg \psi (\mathbf{c})\}$ is a permitted next stage. Thus each constant tuple will fail some formula of each prescribed type.

The union $T^{\ast }=T\cup {\bigcup }_s{\Gamma }_s$ is consistent by the finite character of formal proofs, complete in the expanded language, and has the Henkin witness property. Its term model has closed terms modulo provable equality as elements, and satisfies the truth lemma for a Henkin term model, proved by induction on formulas. It is countable. Every closed term $t$ equals a constant in this model: apply the witness task to $\exists x(x=t)$. Consequently every tuple is represented by a constant tuple and fails a formula of each $p_j$. This proves simultaneous omission.

For arithmetic, the nonstandard element type isIn a model of Peano arithmetic, an element omits this type precisely when it is one of the standard numerals: arithmetic proves that every element at most $\overline{n}$ equals one of $\overline{0},\dots ,\overline{n}$. A model omitting $p_{\infty }$ everywhere is therefore isomorphic to the standard structure $\mathbb{N}$.

For a complete consistent theory $T\supseteq \mathrm{PA}$, this gives the particularly useful equivalenceThe first implication is the omitting types theorem. For the converse, if a consistent $\theta$ over the theory of true arithmetic implied every $x>\overline{n}$, completeness would give $\mathbb{N}\models \exists x\theta (x)$. A standard witness $m$ contradicts the implication $\theta \to x>\overline{m}$.

Completeness matters in this formulation. One must not claim that $p_{\infty }$ is automatically nonprincipal over an arbitrary incomplete arithmetic theory. For example, assuming consistency of Peano arithmetic, the formula saying that $x$ is the least code of a proof of a contradiction is consistent with that theory, by Gödel second incompleteness theorem, and implies $x>\overline{n}$ for each standard $n$. It makes $p_{\infty }$ principal over that incomplete theory, although its standard model still omits the type. The theorem is a sufficient omission criterion, not a necessary one for arbitrary partial types over incomplete theories.

For a first-order theory $T$ in a first-order language $L$, a complete $n$-type is a maximal $T$-consistent set $p(x_1,\dots ,x_n)$ of formulas whose free variables lie among $x_1,\dots ,x_n$. Equivalently, it chooses exactly one of $\phi$ and $\neg \phi$ for every such formula while remaining consistent with $T$.

An isolated type $p$ is isolated by a formula $\theta (\bar{x})$ when $T\cup \{\exists \bar{x}\theta (\bar{x})\}$ is consistent andfor every $\phi \in p$. The type is an omitted type in an $L$-structure $M$ when no tuple $\bar{a}\in M^n$ satisfies every formula in $p$.

The omitting types theorem states that if $T$ is a consistent theory in a countable language and $(p_i{)}_{i\in \mathbb{N}}$ is a countable family of nonisolated finite-arity types, then $T$ has a countable model omitting every $p_i$.

Suppose first that $T$ is aleph-zero-categorical. If a type in some $S_n(T)$ were nonisolated, the omitting types theorem would produce a countable model omitting it, while a countable elementary submodel of a model realizing it would be another countable model. This contradicts categoricity. Thus every type is isolated. The compact Stone space $S_n(T)$ is then discrete and therefore finite.

Conversely, if every $S_n(T)$ is finite, every type is isolated. Every countable model is consequently atomic, and part i says that any two countable models are isomorphic. This proves the Ryll-Nardzewski theorem.

Take the parameter-free complete typeof the nonstandard prime constructed in part (i). It is first-order consistent and complete because it consists of exactly the logical formulas true of an actual element in a first-order model of $T$. It contains $x\ne \bar{a}$ for every integer $a$, and consequently no element of $\mathcal{Z}$ realizes it. ThusIt is necessarily a nonprincipal complete type. If a first-order consistent logical formula isolated it, completeness of $T$ would force the existential closure of that logical formula to hold in every first-order model of $T$, including $\mathcal{Z}$; a witness there would realize the partial type, a contradiction. This connects the explicit omission with the hypothesis of the omitting types theorem.

Use $AC{F}_0$, the complete theory of algebraically closed fields of characteristic zero. Its quantifier elimination is a standard characterization of this complete theory. Algebraically closed fields of a fixed characteristic are classified up to isomorphism by transcendence degree over their prime field.

For such a field $K$,when the transcendence degree is infinite, while finite transcendence degree also gives a countable field. This follows by counting rational functions in a transcendence basis and then algebraic elements over that field. Thus every first-order model of cardinality ${\aleph }_1$ has transcendence degree ${\aleph }_1$, and the classification gives a unique such first-order model.

On the other hand $\overline{\mathbb{Q}}$ and an algebraic closure of $\mathbb{Q}(t)$ are countably infinite first-order models with transcendence degrees zero and one, so are not isomorphic. HenceThe transcendental complete one-type consists of $f(x)\ne 0$ for every nonzero polynomial over $\mathbb{Q}$. Quantifier elimination makes it complete. It is nonprincipal: any parameter-free one-variable logical formula containing a transcendental element defines a cofinite set, hence contains algebraic elements as well and cannot isolate this partial type. The first-order model $\overline{\mathbb{Q}}$ omits it, concretely illustrating the omitting types theorem. The existence of infinitely many algebraic complete one-types, together with this nonprincipal complete type, also agrees with the failure of the Ryll-Nardzewski finiteness condition.

Reuse the complete free-bijection theory from part (e). Quantifier elimination shows that every one-variable atomic statement is already decided by the no-finite-cycle axioms. Thus there is exactly one complete one-type, isolated by $x=x$.

For two logical variables, each integer $k$ gives a different complete type isolated byThere is also the complete typesaying that the two elements lie in different orbits. These exhaust the possibilities by quantifier elimination. In particularThe last complete type is a nonprincipal complete type. Any logical formula uses only finitely many integer offsets after quantifier elimination; a pair in a single orbit with a sufficiently different offset agrees with a different-orbit pair on those tests. Hence no single logical formula can isolate $p_{\infty }$.

The one-orbit first-order model $(\mathbb{Z},f(n)=n+1,g(n)=n-1)$ omits $p_{\infty }$, while a two-orbit first-order model realizes it. This illustrates the omitting types theorem and shows concretely why finitely many complete one-types alone cannot replace the all-arities condition in Ryll-Nardzewski.

The Ryll-Nardzewski theorem says that for a complete theory $T$ in a countable first-order language with infinite first-order models, the following are equivalent: $T$ is ${\aleph }_0$-categorical; for every positive integer $n$, the set $S_n(T)$ of complete parameter-free $n$-types is finite; every such finite-arity complete type is isolated by a logical formula. The countable-language hypothesis and the requirement for every finite arity are important.

The omitting types theorem says that, for a first-order consistent complete theory in a countable first-order language, a countable family of nonprincipal partial types in finite tuples of logical variables can all be omitted in a countable first-order model. Here nonprincipal means that no logical formula first-order consistent with the first-order theory implies every logical formula of the partial type. Omission means that no tuple in the constructed first-order model satisfies all logical formulas of that partial type. The complete one-type version is the special case of one partial type in one logical variable.

A complete $n$-type over $T$ is a maximal set $p(\bar{x})$ of formulas in $n$ variables consistent with $T$; it decides each such formula or its negation. A partial type drops maximality. A tuple realizes the type if it satisfies every member. A complete type is principal, or isolated, if some formula $\theta (\bar{x})$ consistent with $T$ implies every member of the type modulo $T$; then $\theta$ itself belongs to that type.

The omitting types theorem says that in a countable first-order language, a consistent theory has a countable model omitting a specified nonprincipal type; more generally a countable family of nonprincipal types can be omitted simultaneously. In the present complete-theory setting it applies directly to complete nonisolated types. “Omitted” means that no tuple in the model realizes all formulas of the type, even though each finite subset is compatible with the theory.

A model is prime if it has an elementary embedding into every model of $T$. A model is atomic if every finite tuple realizes an isolated complete type over the empty set.

If $A$ is prime, the downward Löwenheim-Skolem theorem gives a countable model $M$ of $T$, and an elementary embedding $A\to M$ makes $A$ countable. If a tuple of $A$ realized a nonisolated type, the omitting types theorem would give a model of $T$ omitting that type. The prime embedding into it would preserve the tuple's full type and realize the omitted type, a contradiction. Thus a prime model is countable and atomic.

Conversely enumerate a countable atomic model as $a_0,a_1,\dots$, and take any $B\models T$. Build finite partial elementary maps into $B$. Suppose the current tuple $\bar{a}$ maps to $\bar{b}$. Choose a formula $\theta (\bar{x},y)$ isolating the type of $(\bar{a},a_n)$. The assertion $\exists y\theta (\bar{a},y)$ holds in $A$, so its counterpart holds at $\bar{b}$ in $B$ by partial elementarity. Choose a witness $b_n$. Since $\theta$ isolates the entire extended tuple type, the extended map is elementary on its finite domain; its equality formulas ensure distinct Elements remain distinct. The union is a total elementary embedding $A\to B$. The empty initial tuple works because $T$ is complete. Hence