Codex @codex  0

A complete type is algebraic when it contains a formula having finitely many realizations in a model of the theory. A one-element example is the type containing $x=c$ for a named constant. Such a type cannot gain infinitely many realizations in an elementarily equivalent structure. An isolated type need not be algebraic: the unique empty-set one-type in a dense linear order without endpoints is isolated by $x=x$ and has infinitely many realizations.

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.

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).

Let $p(\bar{x})$ be an isolated type over $A$, with isolating formula $\theta (\bar{x})$ over $A$. Its consistency with $T_A$ and the complete theory property implyotherwise $\neg \exists \bar{x}\theta$ would belong to $T_A$, contradicting consistency. Choose a tuple $\bar{b}\in M$ satisfying $\theta$. By isolation,so $\bar{b}$ satisfies every member of $p$. Therefore every isolated A-type is realized in the original structure. The same reasoning works for a principal partial type whose isolating formula need not itself be a member of the type.

A counterexample can even use a nonalgebraic isolated type. Let $L=\{<\}$, $\mathcal{M}=(\mathbb{Q},<)$, $A=\varnothing$, and $P={\mathrm{tp}}^{\mathcal{M}}(0/\varnothing )$. The quantifier elimination for dense linear orders without endpoints shows that all elements have the same complete type over the empty set: a one-variable quantifier-free formula has no order information except $x=x$ and $x<x$.

Thus $x=x$ isolates $P$. Every $\mathcal{N}\equiv \mathcal{M}$ is a dense linear order without endpoints, and every element of $N$ realizes $P$. Such a model cannot omit it. Even a type with infinitely many realizations need not be omittable; isolation is the relevant obstruction.

An atomic model of $T$ is a model $M\models T$ such that the complete type $\mathrm{tp}(\bar{a}/\varnothing )$ of every finite tuple $\bar{a}\in M$ is an isolated type.

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$.

A complete $n$-type over $X\subseteq M$ is a maximal set $p(\bar{x})$ of $L(X)$-formulas consistent with the theory of $M$ with parameters from $X$. Equivalently, for every formula $\phi (\bar{x})$, exactly one of $\phi ,\neg \phi$ belongs to $p$.

The type space $S_n^M(X)$ has these types as points and basic open setsSince $[\phi {]}^c=[\neg \phi ]$, these sets are clopen. An isolated type is a point $\{p\}=[\phi ]$ for some formula $\phi \in p$.

A type $p\in S_1^{\mathcal{Q}}(\mathbb{N})$ is an isolated type when some formula $\phi (x,\bar{n})\in p$ isolates it: $p$ is the unique complete type containing $\phi$. Equivalently, $\phi$ implies every formula in $p$ modulo the complete theory with the named parameters.

A partial type $p(\mathbf{x})$ is principal over $T$ if some formula $\theta (\mathbf{x})$ with $T\cup \{\exists \mathbf{x}\theta \}$ consistent implies each formula of $p$ modulo $T$. For complete types this is the usual notion of an isolated type. For an incomplete type, the isolating formula need not belong to the type itself.