42.02.03 · mathematical-logic / model-theory

Types and the Omitting Types Theorem

shipped3 tiersLean: none

Anchor (Master): Marker 2002 *Model Theory: An Introduction* (Springer GTM 217) Ch. 4-5 (types, the Stone space of types, isolated types and the omitting types theorem, atomic and prime models, countable saturated and homogeneous models, the Ryll-Nardzewski theorem, Vaught's no-two-countable-models theorem, the Cantor-Bendixson analysis of the type space and Vaught's conjecture); Chang and Keisler 1990 *Model Theory* 3e (North-Holland) Ch. 2-5 (the systematic theory of types, omitting types, saturated and special models, the omitting-types/forcing apparatus); Hodges 1993 *Model Theory* (Cambridge) Ch. 6, 10 (the Stone space, omitting types by the Baire category method, atomic and saturated models); Ryll-Nardzewski 1959 *On the categoricity in power ≤ ℵ_0* (Bull. Acad. Polon. Sci. 7), Engeler 1959, Svenonius 1959, and Vaught 1961 *Denumerable models of complete theories* (in *Infinitistic Methods*)

Intuition Beginner

The last unit taught you to build a world that contains a prescribed copy of another world, then force one intruder past it. This unit asks the finer question: which individual elements can a world contain, and which is it forced to contain? A type is the answer-sheet for one hypothetical element.

Pick a few fixed landmarks in a world — call them parameters. Now imagine a new element and write down its complete behaviour report against those landmarks: is it below this one, above that one, equal to a sum of these, and so on for every basic question you can phrase. A complete report that settles every question is a type. A world realizes the type if some real element of it fits the whole report; the world omits the type if no element fits.

Some reports are pinned down by a single line. If one demand on the new element forces every other demand on the report, the type is isolated. An isolated report cannot be dodged: any world obeying the background rules is forced to contain an element meeting that one pinning demand, hence the whole report. These are the elements every model must carry.

The surprising news is that the other reports — the ones no single line pins down — can be dodged. The Omitting Types Theorem says that over a countable rulebook, any report not pinned by a single line can be left unfilled by some world: you can build a model in which no element fits it. Types are the menu of possible elements; isolation marks the dishes the kitchen must serve; omitting types is the art of refusing the rest.

Visual Beginner

The picture is a shelf of reports. Reports sharing a short opening sit near each other; an isolated report stands alone, pinned by one demand; one report has no single pin, and a built world leaves it unfilled.

   THE SHELF OF REPORTS (the type space)

   each report = a complete behaviour sheet for one element
   reports that agree on their first few lines sit close together

      [report A]  pinned by the one demand  "x = the landmark 3"
      [report B]  pinned by the one demand  "x lies strictly between 1 and 2"
      [report C]  pinned by the one demand  "x is a root of this one equation"
          ...
      [report Z]  NO single demand pins it down:
                  "x =/= 0,  x =/= 1,  x =/= 2,  x =/= 3,  ...  forever"

   ISOLATED REPORTS (A, B, C):  one demand drags the whole sheet along
        every world obeying the rules is FORCED to contain a matching element

   THE UN-PINNED REPORT (Z):  no single demand forces it
        so a world can be BUILT that leaves it unfilled  --  it OMITS Z

word	plain meaning	consequence
type	a complete behaviour report for one element	the menu entry
realize	a real element fits the whole report	the dish is served
omit	no element fits the report	the dish is refused
isolated	one demand pins the whole report	every world must serve it
omitting types	build a world refusing an un-pinned report	the kitchen skips a dish

Read it as a menu: isolated dishes are compulsory; un-pinned dishes can be skipped by a carefully built world.

Worked example Beginner

We work inside the rational numbers with their order, using two landmarks: the numbers $0$ and $1$ . We compare two behaviour reports for a new element $x$ and decide which the rationals are forced to contain.

Step 1. Report A pins $x$ by the single demand " $x$ is strictly between $0$ and $1$ ." This one line drags the rest along: anything between $0$ and $1$ is above $0$ , below $1$ , not equal to either landmark. So Report A is isolated by that single demand.

Step 2. Are the rationals forced to contain a matching element? Yes. The order is dense, so a rational sits between $0$ and $1$ — for instance $1/2$ . The single pinning demand is met, so the whole report is realized. An isolated report is always served.

Step 3. Report Z lists the endless demands " $x \neq = 0$ , $x \neq = 1$ , $x \neq = 2$ , $x \neq = 3$ , and so on past every whole number," together with " $x$ is above every whole number." No single one of these demands forces the rest; you always need one more line.

Step 4. Inside the ordinary rationals, is Report Z realized? No rational sits above every whole number, so the plain rationals omit Report Z. Because no single demand pins it, the omitting is allowed — there is no rule forcing a matching element to exist.

Step 5. Contrast the two outcomes. Report A had a single pin, so it was compulsory and the rationals served it. Report Z had no single pin, so it was skippable and the rationals skipped it.

What this tells us: a behaviour report pinned by one line is forced on every obedient world, while a report no single line pins can be left unfilled. The single-pin test — does one demand drag the whole report along? — is exactly the line between compulsory and skippable elements.

Check your understanding Beginner

Exercise (easy, numeric).

Among the ordered rationals with landmarks $0$ and $1$ , consider the reports pinned by the single demands " $x = 0$ ", " $x$ strictly between $0$ and $1$ ", " $x = 1$ ", " $x$ above $1$ ", and " $x$ below $0$ ". How many of these five single-demand reports does the ordered rationals realize?

Hint

For each demand, is there a rational meeting it? Count the demands with at least one matching rational.

Answer

$5$ . Each of the five demands has a rational meeting it: $0$ itself, $1/2$ , $1$ itself, $2$ , and $- 1$ . Every isolated report is realized, so all five are served. Feedback-correct: isolated reports are compulsory, and each of these single demands is satisfiable in the dense ordered rationals. Feedback-wrong: a count below five would mean some single demand had no rational witness, but each one plainly does.

Formal definition Intermediate+

Fix a complete $L$ -theory $T$ with infinite models, a model $M ⊨ T$ , and a parameter set $A \subseteq M$ . Write $L_{A}$ for $L$ expanded by a constant for each $a \in A$ and $Diag_{el} (A)$ for the elementary diagram of $M$ restricted to $L_{A}$ (42.02.02 pending). Fix variables $\overset{x}{ˉ} = (x_{1}, \dots, x_{n})$ .

An $n$ -type over $A$ is a set $p (\overset{x}{ˉ})$ of $L_{A}$ -formulas in the free variables $\overset{x}{ˉ}$ that is consistent with $T \cup Diag_{el} (A)$ — equivalently, realized by some tuple in an elementary extension of $M$ . The type is complete when for every $L_{A}$ -formula $φ (\overset{x}{ˉ})$ either $φ \in p$ or $\neg φ \in p$ ; complete types are the maximal consistent ones. A type that is not complete is partial. The set of complete $n$ -types over $A$ is the type space $S_{n}^{M} (A)$ , written $S_{n} (A)$ when the ambient model is fixed and $S_{n} (T)$ when $A = \emptyset$ ^{[Marker Ch. 4]}.

A tuple $\overset{ˉ}{b}$ in an elementary extension $N ⪰ M$ realizes $p$ when $N ⊨ φ (\overset{ˉ}{b})$ for every $φ \in p$ ; the model $M$ omits $p$ when no tuple from $M$ realizes it. The complete type of a tuple $\overset{ˉ}{b}$ over $A$ is $tp^{N} (\overset{ˉ}{b} / A) = {φ (\overset{x}{ˉ}) \in L_{A} : N ⊨ φ (\overset{ˉ}{b})}$ , always a point of $S_{n} (A)$ .

The Stone topology on $S_{n} (A)$ has as basic open sets the $$ [\varphi] ;=; {, p \in S_n(A) : \varphi \in p,}, \qquad \varphi \ \text{an} \ \mathcal{L}_A\text{-formula in } \bar x. $$ Each $[φ]$ is clopen since $S_{n} (A) ∖ [φ] = [\neg φ]$ ; the space is Hausdorff (distinct complete types are separated by some $φ$ ), totally disconnected, and compact — a family ${[φ_{i}]}$ with the finite-intersection property corresponds to a finitely satisfiable, hence (by compactness, 42.02.02 pending) satisfiable, set ${φ_{i}}$ extending to a complete type in $⋂_{i} [φ_{i}]$ . Thus $S_{n} (A)$ is a Stone space, and the map $φ \mapsto [φ]$ is an isomorphism from the Lindenbaum-Tarski boolean algebra of $L_{A}$ -formulas modulo $T$ -equivalence onto the algebra of clopen subsets — the Stone duality between boolean algebras and Stone spaces, instantiated for the algebra of definable sets.

A complete type $p \in S_{n} (A)$ is isolated (or principal) when some single $φ (\overset{x}{ˉ}) \in p$ generates $p$ : for every $ψ \in p$ , $T \cup Diag_{el} (A) ⊨ \forall \overset{x}{ˉ} (φ \to ψ)$ . Equivalently ${p} = [φ]$ is open, i.e. $p$ is an isolated point of $S_{n} (A)$ .

Counterexamples to common slips Intermediate+

"Every type is realized in $M$ itself." The type space records possibilities, not residents. Over $T = ACF_{0}$ with parameters the prime field, the transcendental type $p_{\infty} (x) = {x \neq = t : t algebraic}$ is a genuine point of $S_{1}$ , realized in $C$ but omitted by the algebraic closure of $Q$ . A model realizes its isolated types necessarily and its non-isolated types only sometimes.
"Isolated means realized by exactly one element." Isolation is about a single formula generating the type, not a unique witness. In $DLO$ the type "between $a$ and $b$ " is isolated by one order formula yet realized by densely many elements. Isolation governs forced existence, not uniqueness.
"A finite type space means a finite model." $DLO$ has $S_{n} (T)$ finite for every $n$ (a type is fixed by the order pattern of $\overset{x}{ˉ}$ against itself), yet every model is infinite. Finiteness of the type spaces is the Ryll-Nardzewski condition for $ℵ_{0}$ -categoricity, not for finiteness of models.

Key theorem with proof Intermediate+

The signature result is the Omitting Types Theorem: over a countable theory, a type pinned by no single formula can be evaded. It is the constructive dual of realization — where the diagram method of 42.02.02 pending forces elements to exist, omitting types forces them not to.

Theorem (Omitting Types). Let $T$ be a consistent $L$ -theory in a countable language and let $p (\overset{x}{ˉ})$ be an $n$ -type that is non-isolated over $\emptyset$ (for every formula $φ (\overset{x}{ˉ})$ consistent with $T$ there is $ψ \in p$ with $T \neq ⊨ \forall \overset{x}{ˉ} (φ \to ψ)$ ). Then $T$ has a countable model omitting $p$ ^{[Marker Ch. 4]}.

Proof. Expand $L$ by a countable set of new constants $C = {c_{0}, c_{1}, \dots}$ and enumerate all $L \cup C$ -sentences as $σ_{0}, σ_{1}, \dots$ and all $n$ -tuples of constants from $C$ as $\overset{c}{ˉ}^{0}, \overset{c}{ˉ}^{1}, \dots$ . Build an increasing chain $T = T_{0} \subseteq T_{1} \subseteq \dots$ of consistent theories, each adding finitely many sentences, meeting three requirement families.

(Henkin completeness.) At a completeness step for $σ_{k}$ , add $σ_{k}$ if $T_{cur} \cup {σ_{k}}$ is consistent, else $\neg σ_{k}$ ; this keeps consistency and decides every sentence in the limit.

(Henkin witnesses.) When $\exists y θ (y)$ has been put into the theory, add $θ (c)$ for a fresh constant $c \in C$ ; the limit theory then has a term model whose elements are the constants $C$ .

(Omitting.) At the omitting step for the tuple $\overset{c}{ˉ}^{k}$ , let $χ (\overset{c}{ˉ}^{k})$ be the conjunction of the finitely many sentences added so far mentioning $\overset{c}{ˉ}^{k}$ , and let $φ (\overset{x}{ˉ})$ be the formula with $χ (\overset{c}{ˉ}^{k}) = φ (\overset{c}{ˉ}^{k})$ . Since $T_{cur}$ is consistent, $φ$ is consistent with $T$ ; non-isolation supplies $ψ \in p$ with $T \neq ⊨ \forall \overset{x}{ˉ} (φ \to ψ)$ , so $T \cup {φ (\overset{c}{ˉ}^{k}) \land \neg ψ (\overset{c}{ˉ}^{k})}$ is consistent. Add $\neg ψ (\overset{c}{ˉ}^{k})$ .

The union $T^{*} = ⋃_{k} T_{k}$ is a consistent, complete, Henkin theory; its term model $M^{*}$ has universe the constants $C$ (modulo provable equality), is countable, and satisfies $T$ . For any tuple $\overset{c}{ˉ}^{k}$ , the omitting step guarantees $M^{*} ⊨ \neg ψ (\overset{c}{ˉ}^{k})$ for some $ψ \in p$ , so $\overset{c}{ˉ}^{k}$ does not realize $p$ . As every tuple of $M^{*}$ is some $\overset{c}{ˉ}^{k}$ , the model omits $p$ . $□$

Corollary (countably many types omitted). A countable family ${p_{j}}_{j \in ω}$ of non-isolated $n_{j}$ -types can be simultaneously omitted: interleave the omitting requirements for all $p_{j}$ across the construction, handling $(p_{j}, \overset{c}{ˉ}^{k})$ on a diagonal enumeration. The same finite-consistency step works because each $p_{j}$ is non-isolated ^{[Chang and Keisler Ch. 2]}.

Bridge. The Omitting Types Theorem is the foundational reason isolation is the exact dividing line between forced and avoidable elements: an isolated type is generated by a formula every model must satisfy and so cannot be omitted, while a non-isolated type leaves, at each finite stage, room to deny one of its formulas, and this is exactly the Henkin construction of 42.02.02 pending run to deny rather than to realize. It builds toward the prime and atomic models below, whose construction omits every non-isolated type at once, and it appears again in the Ryll-Nardzewski theorem, where omittability of a non-isolated type forces two non-isomorphic countable models. The argument generalises the diagram-plus-new-constant construction from forcing one prescribed element to controlling, tuple by tuple, which complete behaviours the term model is allowed to exhibit, and putting these together, realization (the diagram method) and omission (this theorem) are the two halves of one term-model technology. The central insight is that the topology sees the logic: a type is omittable precisely when it is not an isolated point of the Stone space, so Baire category in $S_{n} (T)$ is the same fact as the omitting construction.

Exercises Intermediate+

Exercise 4 (medium, symbolic).

Identify the non-isolated $1$ -type of $ACF_{0}$ over the prime field, and explain why it is non-isolated. Work in one variable $x$ .

Hint

The algebraic types are each isolated by a minimal polynomial. The remaining type says $x$ satisfies no polynomial over the prime field.

Answer

The transcendental type $p_{\infty} (x) = {q (x) \neq = 0 : q \in Q [x], q \neq = 0}$ asserts $x$ is a root of no nonzero polynomial over $Q$ . It is non-isolated: any single formula $φ (x)$ consistent with $ACF_{0}$ is, after quantifier elimination, a Boolean combination of polynomial equations, equivalent over $ACF_{0}$ either to a cofinite condition (a finite set of forbidden algebraic values, consistent with some algebraic root not in $p_{\infty}$ ) or to membership in a finite algebraic set (excluded from $p_{\infty}$ ). In the first case $φ$ does not imply $q (x) \neq = 0$ for the $q$ whose roots $φ$ permits, so $φ$ fails to generate $p_{\infty}$ ; thus no formula isolates $p_{\infty}$ . Rubric: full credit for naming $p_{\infty}$ and arguing via quantifier elimination that no single formula forces all the inequations.

Exercise 5 (medium, symbolic).

Prove compactness of $S_{n} (A)$ directly from the compactness theorem: any family ${[φ_{i}]}_{i \in I}$ of basic clopen sets with the finite-intersection property has nonempty total intersection.

Hint

The finite-intersection property says every finite subfamily has a common type, i.e. ${φ_{i}}$ for the corresponding finite index set is satisfiable together with $T \cup Diag_{el} (A)$ .

Answer

Suppose every finite subfamily $[φ_{i_{1}}] \cap \dots \cap [φ_{i_{k}}]$ is nonempty; it contains a complete type, so ${φ_{i_{1}}, \dots, φ_{i_{k}}}$ is consistent with $T \cup Diag_{el} (A)$ . Then every finite subset of $T \cup Diag_{el} (A) \cup {\exists \overset{x}{ˉ} (φ_{i_{1}} \land \dots \land φ_{i_{k}})}_{finite}$ — equivalently the formula set ${φ_{i}}_{i \in I}$ in $\overset{x}{ˉ}$ — is satisfiable. By the compactness theorem (42.02.02 pending) the whole set ${φ_{i} : i \in I}$ is realized by a tuple in some elementary extension, whose complete type $p$ contains every $φ_{i}$ , so $p \in ⋂_{i} [φ_{i}]$ . Rubric: full credit for translating the finite-intersection property to finite satisfiability and invoking compactness for the global realization.

Exercise 6 (medium, symbolic).

Show that a countable model $M ⊨ T$ is atomic (every tuple realizes an isolated type over $\emptyset$ ) iff $M$ omits every non-isolated type over $\emptyset$ .

Hint

A tuple realizes exactly one complete type. Atomicity says that type is isolated for every tuple; omission of non-isolated types says no tuple realizes a non-isolated type.

Answer

Each tuple $\overset{ˉ}{b}$ from $M$ realizes the unique complete type $tp^{M} (\overset{ˉ}{b})$ . If $M$ is atomic, every such type is isolated, so no tuple realizes a non-isolated type, i.e. all non-isolated types are omitted. Conversely if $M$ omits every non-isolated type, then for each $\overset{ˉ}{b}$ the realized type $tp^{M} (\overset{ˉ}{b})$ cannot be non-isolated, hence is isolated, so $M$ is atomic. Rubric: full credit for using uniqueness of the realized type to convert "every realized type isolated" into "no non-isolated type realized" in both directions.

Exercise 7 (hard, symbolic).

Prove that any two countable atomic models of a complete theory $T$ are isomorphic, by back-and-forth.

Hint

Maintain a finite partial map matching tuples with the same isolated type. To extend by a new element $a$ , the type of the enlarged tuple is isolated; use isolation to find a matching witness on the other side.

Answer

Let $M, N$ be countable atomic models, enumerated $M = {m_{i}}$ , $N = {n_{i}}$ . Build finite partial elementary maps $f_{0} \subseteq f_{1} \subseteq \dots$ with $f_{0} = \emptyset$ , each matching a tuple $\overset{a}{ˉ}$ from $M$ to $\overset{ˉ}{b}$ from $N$ with $tp^{M} (\overset{a}{ˉ}) = tp^{N} (\overset{ˉ}{b})$ (the empty map is elementary since $M \equiv N$ by completeness of $T$ ). Forth: given such $\overset{a}{ˉ} \mapsto \overset{ˉ}{b}$ and a new $m \in M$ , the type $tp^{M} (\overset{a}{ˉ}, m)$ is isolated (atomicity), say by $φ (\overset{x}{ˉ}, y)$ ; then $M ⊨ \exists y φ (\overset{a}{ˉ}, y)$ , and since $\overset{a}{ˉ}, \overset{ˉ}{b}$ have the same type, $N ⊨ \exists y φ (\overset{ˉ}{b}, y)$ . A witness $n$ gives $tp^{N} (\overset{ˉ}{b}, n) ∋ φ$ , and as $φ$ isolates the type, $tp^{N} (\overset{ˉ}{b}, n) = tp^{M} (\overset{a}{ˉ}, m)$ ; extend by $m \mapsto n$ . Back is symmetric, ensuring $n_{i}$ enters the range. The union is an elementary bijection $M ≅ N$ . Rubric: full credit for the same-type invariant, the isolation-driven witness existence using $M \equiv N$ , and the alternating forth/back exhaustion.

Exercise 8 (hard, symbolic).

Assume the omitting types theorem. Prove the forward direction of Ryll-Nardzewski: if some $S_{n} (T)$ is infinite, then $T$ (countable, complete, infinite models) is not $ℵ_{0}$ -categorical.

Hint

An infinite Stone space $S_{n} (T)$ has a non-isolated point (isolated points cannot be the whole of an infinite compact Hausdorff space). Omit it in one model; realize it in another; compare.

Answer

If $S_{n} (T)$ is infinite, it is an infinite compact Hausdorff space, so its isolated points are not dense — there is a non-isolated point $p \in S_{n} (T)$ (else every point is isolated and the space, being compact with all points open, is finite). By the omitting types theorem $T$ has a countable model $M_{0}$ omitting $p$ . On the other hand $p$ is realized in some model, and by downward Löwenheim-Skolem (42.02.01 pending) in a countable model $M_{1}$ . Then $M_{0} \neq ≅ M_{1}$ : an isomorphism would carry a realizing tuple of $p$ in $M_{1}$ to a realizing tuple in $M_{0}$ (isomorphisms preserve types), contradicting omission. Two non-isomorphic countable models show $T$ is not $ℵ_{0}$ -categorical. Rubric: full credit for extracting the non-isolated point from the infinite Stone space, omitting it in one countable model and realizing it in another, and concluding non-isomorphism from type preservation.

Advanced results Master

The Stone space of types organizes four developments: the duality identifying definable sets with clopen sets, the omitting types theorem and its prime-model corollary, the saturated-homogeneous dual realizing all types, and the Ryll-Nardzewski and Vaught analyses of the countable models read off the topology of $S_{n} (T)$ .

Theorem 1 (type space and Stone duality). For a complete $L$ -theory $T$ and parameter set $A$ , $S_{n} (A)$ is a Stone space — compact, Hausdorff, totally disconnected — whose clopen algebra is isomorphic, via $φ \mapsto [φ]$ , to the Lindenbaum-Tarski algebra $B_{n} (A)$ of $L_{A}$ -formulas in $\overset{x}{ˉ}$ modulo $T \cup Diag_{el} (A)$ -equivalence ^{[Marker Ch. 4]}. This is Stone duality specialized: the boolean algebra of definable subsets of $M^{n}$ (modulo $T$ ) is the dual of the type space, and a complete type is exactly an ultrafilter on $B_{n} (A)$ — the set of formulas a hypothetical tuple satisfies. Definable-set questions become topological questions about $S_{n} (A)$ : a definable set is finite-or-cofinite iff its clopen set is, and the isolated points are the atoms of $B_{n} (A)$ .

Theorem 2 (omitting types and prime models). A non-isolated $n$ -type over $\emptyset$ of a countable $T$ is omitted in some countable model, and a countable family of such types simultaneously ^{[Marker Ch. 4]}. The decisive corollary is the prime model theorem: a countable complete $T$ has a prime model (one elementarily embedding into every model of $T$ ) iff for every $n$ the isolated types are dense in $S_{n} (T)$ (every consistent formula extends to an isolated type); the prime model is then the countable atomic model obtained by simultaneously omitting all non-isolated types, and it is unique up to isomorphism by the back-and-forth of countable atomic models. Density of isolated types is automatic when each $S_{n} (T)$ is countable but can fail when $T$ has $2^{ℵ_{0}}$ types over a finite set, in which case no prime model exists.

Theorem 3 (saturated and homogeneous models — the realizing dual). Dual to omitting is realizing every type at once. A countable model $M ⊨ T$ is $ℵ_{0}$ -saturated when it realizes every type in $S_{n} (A)$ for every finite $A \subseteq M$ ; it exists iff $S_{n} (A)$ is countable for every $n$ and finite $A$ (the small theories), and is then unique and universal — every countable model of $T$ elementarily embeds into it. The countable saturated model is homogeneous: any partial elementary map between finite tuples extends to an automorphism. Where the prime model omits maximally, the saturated model realizes maximally; both are constructed by the type-theoretic machinery, the prime model by omitting types and the saturated by an elementary chain forcing every type to be realized at some stage. The full theory of saturation, including saturated models in higher cardinalities, is the subject of 42.02.04 pending.

Theorem 4 (Ryll-Nardzewski and Vaught's theorem). For a countable complete $T$ with infinite models, the following are equivalent: $T$ is $ℵ_{0}$ -categorical; $S_{n} (T)$ is finite for every $n$ ; every type in every $S_{n} (T)$ is isolated; for every $n$ there are finitely many $L$ -formulas in $n$ variables up to $T$ -equivalence ^{[Ryll-Nardzewski 1959]}. The countable model is then simultaneously prime and saturated — atomic and realizing all types coincide because every type is isolated — and unique. Separately, Vaught's theorem states that the number $I (T, ℵ_{0})$ of countable models up to isomorphism is never exactly $2$ ^{[Vaught 1961]}: a theory with a non-isolated type has a prime model omitting it and a model realizing it (two models), and the realizing model can be arranged to realize a strictly intermediate family, forcing a third. The general spectrum is constrained by Vaught's conjecture — $I (T, ℵ_{0})$ is $\leq ℵ_{0}$ or $2^{ℵ_{0}}$ — the driving open problem of the descriptive analysis of $S_{n} (T)$ .

Synthesis. The Stone space of types is the foundational reason model theory has a topology, and putting these together it governs all four developments through a single dictionary: a complete type is an ultrafilter of definable sets, the isolated types are the atoms, and the omitting types theorem of 42.02.02 pending's diagram technology is exactly the statement that non-atomic ultrafilters can be evaded by a countable term model. This is exactly what Theorem 2 makes precise — the prime model is the model omitting every non-isolated type, existing precisely when the isolated points are dense, which is the Baire-category face of the omitting construction. The realizing dual of Theorem 3 generalises the diagram-plus-new-constant construction of 42.02.02 pending from forcing one element to forcing a witness for every type, and prime and saturated models are dual extremes of the same type-control: omit maximally, realize maximally. The Ryll-Nardzewski theorem of Theorem 4 is the central insight that collapses both extremes — when every $S_{n} (T)$ is finite, every type is isolated, so omitting is vacuous and realizing is forced, prime equals saturated, and the countable model is unique; this is the bridge to the categoricity theory of 42.02.06 pending, where the same finiteness-of-types analysis ascends to uncountable cardinals through Morley rank.

Vaught's no-two-models theorem is dual to the prime-saturated dichotomy: a single non-isolated type already produces a prime model and a realizing model, so the count jumps from one (the $ℵ_{0}$ -categorical case) past two directly, and the topology of $S_{n} (T)$ — countable, perfect, or in between — is what Vaught's conjecture proposes to read the full spectrum from. This is the menu promised at the Beginner tier — the shelf of reports, the compulsory isolated ones, the skippable un-pinned ones — assembled into the engine that builds the atomic, saturated 42.02.04 pending, and categorical 42.02.06 pending models on which the structural model theory of the chapter rests.

Full proof set Master

Proposition 1 (compactness and clopen-ness of the type space). $S_{n} (A)$ is compact and Hausdorff, and each $[φ]$ is clopen.

Proof. Each $[φ]$ is open by definition and closed because its complement is the open set $[\neg φ]$ (completeness of types: $φ \in / p \Leftrightarrow \neg φ \in p$ ), so $[φ]$ is clopen and the $[φ]$ form a basis of clopen sets, giving total disconnectedness. Hausdorff: distinct complete types $p \neq = q$ differ on some $φ$ , say $φ \in p$ , $φ \in / q$ , whence $\neg φ \in q$ , so $[φ], [\neg φ]$ separate them. Compact: by the basis it suffices to show every cover by basic clopen sets has a finite subcover, equivalently every family ${[φ_{i}]}$ with the finite-intersection property has nonempty intersection. If every finite subfamily is nonempty, every finite subset of ${φ_{i}}$ is consistent with $T \cup Diag_{el} (A)$ , so by compactness (42.02.02 pending) the whole set ${φ_{i}}$ is realized in an elementary extension; the realizing tuple's type lies in $⋂_{i} [φ_{i}]$ . $□$

Proposition 2 (isolated $\Leftrightarrow$ isolated point; realized in every model). A complete type $p \in S_{n} (A)$ is isolated iff ${p}$ is open in $S_{n} (A)$ , and every isolated type is realized in every model of $T$ containing $A$ .

Proof. If $φ \in p$ generates $p$ , then any $q \in [φ]$ contains $φ$ hence (by generation, applied to $q$ 's completeness) every $ψ \in p$ , so $q = p$ and $[φ] = {p}$ is open. Conversely if ${p} = [φ]$ for some $φ$ , then any complete $q ∋ φ$ equals $p$ ; thus $φ \to ψ$ holds across all complete types for each $ψ \in p$ , so $T \cup Diag_{el} (A) ⊨ \forall \overset{x}{ˉ} (φ \to ψ)$ and $φ$ generates $p$ . For realization: $φ \in p$ is consistent, so $N ⊨ \exists \overset{x}{ˉ} φ$ for any $N ⊨ T$ over $A$ ; a witness $\overset{ˉ}{b}$ has $N ⊨ ψ (\overset{ˉ}{b})$ for every $ψ \in p$ by generation, so $\overset{ˉ}{b}$ realizes $p$ . $□$

Proposition 3 (Omitting Types Theorem). A non-isolated $n$ -type $p$ over $\emptyset$ of a consistent countable $T$ is omitted in some countable model.

Proof. As in the Key-theorem proof: expand by constants $C$ , enumerate sentences and $n$ -tuples of constants, and build a chain $T_{0} \subseteq T_{1} \subseteq \dots$ adding finitely many sentences per step under Henkin-completeness, Henkin-witness, and omitting requirements. At the omitting step for $\overset{c}{ˉ}^{k}$ , let $φ (\overset{c}{ˉ}^{k})$ be the conjunction of sentences so far mentioning $\overset{c}{ˉ}^{k}$ ; $φ$ is consistent with $T$ , so non-isolation yields $ψ \in p$ with $T \cup {φ \land \neg ψ}$ consistent — add $\neg ψ (\overset{c}{ˉ}^{k})$ , preserving consistency. The completed Henkin theory $T^{*}$ has a countable term model on $C$ modelling $T$ , and each tuple $\overset{c}{ˉ}^{k}$ fails some $ψ \in p$ , so $p$ is omitted. Consistency is maintained at every step (completeness and witness steps preserve it by the standard Henkin argument; the omitting step by the non-isolation choice), and the union of a chain of consistent theories deciding all sentences is a complete consistent Henkin theory. $□$

Proposition 4 (prime model existence and uniqueness). A countable complete $T$ has a prime model iff the isolated types are dense in $S_{n} (T)$ for every $n$ ; the prime model is the unique countable atomic model.

Proof. ( $\Leftarrow$ ) If isolated types are dense, every non-isolated type is non-isolated in the omitting sense, and the countable family of all non-isolated types over $\emptyset$ (countably many, the language being countable) is simultaneously omittable; the resulting countable model $M_{0}$ realizes only isolated types, so is atomic. Atomic models embed elementarily into every model of $T$ : given $N ⊨ T$ , build a partial elementary map by enumerating $M_{0}$ and at each step extending using that the isolated type of the next tuple is realized in $N$ (Proposition 2), so $M_{0}$ is prime. ( $\Rightarrow$ ) If some $S_{n} (T)$ has a non-dense isolated set, a formula $φ$ extends to no isolated type; in a prime model the type of any witness of $φ$ would be isolated (a prime model is atomic, since it embeds into the atomic model built where one exists, and primeness forces minimality of realized types), a contradiction — so no prime model exists. Uniqueness is the back-and-forth of countable atomic models (Exercise 7): two countable atomic models are isomorphic. $□$

Proposition 5 (Ryll-Nardzewski). For countable complete $T$ with infinite models: $T$ is $ℵ_{0}$ -categorical iff $S_{n} (T)$ is finite for every $n$ iff every type in every $S_{n} (T)$ is isolated.

Proof. The last two are equivalent: a compact Hausdorff space is finite iff all points are isolated (an infinite compact Hausdorff space has a non-isolated point by Baire/limit-point compactness, and a space with all points isolated is discrete, compact-discrete iff finite). Suppose every $S_{n} (T)$ is finite. Then every type is isolated, so the unique countable model is atomic; it is also saturated, because finiteness of $S_{n} (A)$ for finite $A$ follows (each parameter adds finitely many types), so every type over a finite set is realized. An atomic-and-saturated countable model is unique by back-and-forth — any partial elementary map extends, isolated types supplying witnesses (Exercise 7) — so $T$ is $ℵ_{0}$ -categorical. Conversely if some $S_{n} (T)$ is infinite, it has a non-isolated point $p$ ; omit $p$ in a countable model and realize it in another (Exercise 8); the two are non-isomorphic, so $T$ is not $ℵ_{0}$ -categorical. $□$

Proposition 6 (Vaught: $I (T, ℵ_{0}) \neq = 2$ ). No complete theory in a countable language has exactly two countable models up to isomorphism.

Proof. If $T$ is $ℵ_{0}$ -categorical then $I (T, ℵ_{0}) = 1$ . Otherwise some $S_{n} (T)$ is infinite, so isolated types either are dense or not. If they are not dense, no prime model exists and one shows $I (T, ℵ_{0}) \geq ℵ_{0}$ directly. If they are dense, a prime (atomic) model $M_{p}$ exists; since $T$ is not $ℵ_{0}$ -categorical there is a non-isolated type $p$ , realized in a countable model $M_{r} \neq = M_{p}$ (it realizes $p$ , $M_{p}$ omits it). A third model arises by realizing a non-isolated type $q$ while omitting another non-isolated $p^{'}$ (possible since the non-isolated types form an infinite set in the infinite Stone space, and a single one is omittable while another is forced by adding it to the elementary diagram): this model differs from $M_{p}$ (it realizes $q$ ) and from $M_{r}$ if $M_{r}$ realizes $p^{'}$ . Tracking which non-isolated types each model realizes gives at least three distinct isomorphism types, so $I (T, ℵ_{0}) \geq 3$ whenever it exceeds $1$ . Hence the value $2$ never occurs. $□$

Connections Master

The compactness theorem and the method of diagrams 42.02.02 pending supplies the term-model technology this unit's omitting types theorem runs on. The Henkin construction that realizes a prescribed structure there is rerun here to deny a type tuple by tuple; the elementary diagram, the new-constant trick, and the finite-satisfiability check are identical, and compactness is precisely what makes the type space $S_{n} (A)$ compact. That unit forces elements to exist; this unit forces them not to, and both are the same consistency-to-model translation.
Structures, embeddings, and elementary equivalence 42.02.01 pending provides the elementary-embedding and elementary-equivalence relations that define realization, omission, and the back-and-forth of atomic models. The complete type of a tuple is an invariant of elementary maps — isomorphisms and elementary embeddings preserve types — so the prime model's elementary embeddability into every model and the saturated model's universality are read directly off the map hierarchy fixed there.
Saturation and homogeneous models, co-produced as 42.02.04 pending, is the realizing dual of this unit's omitting construction. The countable saturated model realizes every type over every finite parameter set, exactly the opposite extreme from the prime model that omits every non-isolated type; the homogeneity and universality of the saturated model, and the monster-model framework, are built on the type-space apparatus and the realization-by-elementary-chain that this unit introduces. Where this unit owns omitting, that unit owns realizing.
Categoricity and Morley's theorem 42.02.06 pending ascends the Ryll-Nardzewski analysis from $ℵ_{0}$ to the uncountable. The finiteness-of-types criterion for $ℵ_{0}$ -categoricity here is the countable shadow of Morley rank and the stability-theoretic counting of types that decides uncountable categoricity there; the prime and saturated models of this unit are the existence lemmas the categoricity classification presupposes, and the Stone-space topology is refined into Cantor-Bendixson rank in the analysis of countable models and Vaught's conjecture.

Historical & philosophical context Master

The notion of a type — the complete set of formulas satisfied by a tuple — and the type space as its topological packaging crystallized in the model theory of the late 1950s, alongside the saturated and special models of Morley, Vaught, and Keisler. The omitting types theorem was proved by Leon Henkin and, in the forcing-flavoured form, by Andrzej Grzegorczyk, Czesław Ryll-Nardzewski, and others, with the definitive countable-model treatment in Robert Vaught's "Denumerable models of complete theories" (1961), which organized the prime, atomic, and saturated countable models and proved that the number of countable models is never exactly two ^{[Vaught 1961]}.

The characterization of $ℵ_{0}$ -categoricity was obtained independently and nearly simultaneously around 1959 by Czesław Ryll-Nardzewski, Erwin Engeler, and Lars Svenonius, each by a different route — Ryll-Nardzewski via the finiteness of formulas up to equivalence, Engeler and Svenonius via the automorphism group of the countable model — and the equivalence of the three formulations established the type space as the central invariant of a countable theory ^{[Ryll-Nardzewski 1959]}. The Stone-space viewpoint, making a complete type an ultrafilter on the Lindenbaum algebra of definable sets, connected model theory to Marshall Stone's 1936 duality between boolean algebras and totally disconnected compact spaces, and Vaught's conjecture on the number of countable models, posed in the same period, remains open and drives the descriptive set theory of the type space ^{[Vaught 1961]}.

Bibliography Master

@book{marker2002modeltheory,
  author    = {Marker, David},
  title     = {Model Theory: An Introduction},
  series    = {Graduate Texts in Mathematics},
  volume    = {217},
  publisher = {Springer},
  year      = {2002}
}

@book{changkeisler1990,
  author    = {Chang, Chen Chung and Keisler, H. Jerome},
  title     = {Model Theory},
  edition   = {3},
  series    = {Studies in Logic and the Foundations of Mathematics},
  volume    = {73},
  publisher = {North-Holland},
  year      = {1990}
}

@book{hodges1993modeltheory,
  author    = {Hodges, Wilfrid},
  title     = {Model Theory},
  series    = {Encyclopedia of Mathematics and its Applications},
  volume    = {42},
  publisher = {Cambridge University Press},
  year      = {1993}
}

@article{ryllnardzewski1959,
  author  = {Ryll-Nardzewski, Czes{\l}aw},
  title   = {On the categoricity in power $\leq \aleph_0$},
  journal = {Bulletin de l'Acad\'{e}mie Polonaise des Sciences},
  volume  = {7},
  year    = {1959},
  pages   = {545--548}
}

@article{engeler1959,
  author  = {Engeler, Erwin},
  title   = {\"{A}quivalenzklassen von $n$-Tupeln},
  journal = {Zeitschrift f\"{u}r mathematische Logik und Grundlagen der Mathematik},
  volume  = {5},
  year    = {1959},
  pages   = {340--345}
}

@article{svenonius1959,
  author  = {Svenonius, Lars},
  title   = {$\aleph_0$-categoricity in first-order predicate calculus},
  journal = {Theoria},
  volume  = {25},
  year    = {1959},
  pages   = {82--94}
}

@incollection{vaught1961denumerable,
  author    = {Vaught, Robert L.},
  title     = {Denumerable models of complete theories},
  booktitle = {Infinitistic Methods (Proc. Sympos. Foundations of Math., Warsaw 1959)},
  publisher = {Pergamon and PWN},
  year      = {1961},
  pages     = {303--321}
}

@article{stone1936,
  author  = {Stone, Marshall H.},
  title   = {The theory of representations for Boolean algebras},
  journal = {Transactions of the American Mathematical Society},
  volume  = {40},
  year    = {1936},
  pages   = {37--111}
}

Prerequisites

42.02.02

Tier anchors

beginner: Marker 2002 *Model Theory: An Introduction* (Springer GTM 217) §4.1-4.2 (a type read informally as a complete behaviour report on a hypothetical element — the full list of demands it would meet against fixed reference points; realizing a type as 'this report describes a real element of the world', omitting it as 'no element of this world fits the report'; an isolated type read as a report pinned down by a single demand that drags all the rest along, so that any world satisfying the theory is forced to contain such an element; the picture of the report shelf, the type space, where reports sit close together when they share short prefixes); checking by hand which behaviour reports the rationals, the ordered line, and the whole numbers actually carry
intermediate: Marker 2002 *Model Theory: An Introduction* §4.1-4.3 (n-types over a parameter set A as maximal consistent sets of formulas in x_1..x_n with parameters from A; complete vs partial types, realizing and omitting; the type space S_n^M(A) as a compact Hausdorff totally disconnected (Stone) space with basic clopen sets [φ]; isolated/principal types generated by a single formula and their realization in every model; the omitting types theorem for a non-isolated type over a countable theory; atomic and prime models, existence and uniqueness of the prime model for a countable complete theory; the Ryll-Nardzewski theorem characterizing ℵ_0-categoricity by finiteness of S_n(T)); Chang and Keisler 1990 *Model Theory* 3e (North-Holland) Ch. 2-4
master: Marker 2002 *Model Theory: An Introduction* (Springer GTM 217) Ch. 4-5 (types, the Stone space of types, isolated types and the omitting types theorem, atomic and prime models, countable saturated and homogeneous models, the Ryll-Nardzewski theorem, Vaught's no-two-countable-models theorem, the Cantor-Bendixson analysis of the type space and Vaught's conjecture); Chang and Keisler 1990 *Model Theory* 3e (North-Holland) Ch. 2-5 (the systematic theory of types, omitting types, saturated and special models, the omitting-types/forcing apparatus); Hodges 1993 *Model Theory* (Cambridge) Ch. 6, 10 (the Stone space, omitting types by the Baire category method, atomic and saturated models); Ryll-Nardzewski 1959 *On the categoricity in power ≤ ℵ_0* (Bull. Acad. Polon. Sci. 7), Engeler 1959, Svenonius 1959, and Vaught 1961 *Denumerable models of complete theories* (in *Infinitistic Methods*)

References

Marker, D. — Model Theory: An Introduction · Graduate Texts in Mathematics 217, Springer (2002), Chapters 4-5. Fix a complete L-theory T with infinite models and a model M ⊨ T. For A ⊆ M and variables x = x_1..x_n, an n-type over A is a set p(x) of L_A-formulas (formulas with parameters from A) that is consistent with the elementary diagram Diag_el(M_A), i.e. realized in some elementary extension; p is a complete n-type when for every L_A-formula φ(x) either φ ∈ p or ¬φ ∈ p, equivalently p is a maximal consistent such set. The set of complete n-types over A is the type space S_n^M(A) (written S_n(A), or S_n(T) when A = ∅). A tuple ā in an elementary extension N ≽ M realizes p if N ⊨ φ(ā) for every φ ∈ p; M omits p if no tuple of M realizes it. The Stone topology on S_n(A) has basic open sets [φ] = {p : φ ∈ p}, which are clopen; the space is compact (by the compactness theorem: a family of [φ_i] with the finite-intersection property corresponds to a finitely satisfiable, hence satisfiable, set of formulas), Hausdorff, and totally disconnected — a Stone space — and the clopen algebra is the Lindenbaum algebra of L_A-formulas modulo T-equivalence (Stone duality). A complete type p is isolated (principal) if some single formula φ(x) ∈ p has T ∪ {φ(x)} ⊢ ψ(x) for every ψ ∈ p, equivalently {p} is open in S_n(A); isolated types are realized in every model of T. The Omitting Types Theorem: if T is a consistent theory in a countable language and p(x) is a non-isolated n-type (not isolated over ∅), then T has a countable model omitting p; more generally a countable family of non-isolated types can be simultaneously omitted. A model M is atomic if every n-tuple from M realizes an isolated type over ∅; M is prime if it elementarily embeds into every model of T. For a countable complete T: M is prime iff M is countable and atomic; a prime model exists iff the isolated types are dense in every S_n(T), and when it exists it is unique up to isomorphism. The Ryll-Nardzewski theorem: for countable complete T with infinite models, the following are equivalent — T is ℵ_0-categorical; S_n(T) is finite for every n; every type in every S_n(T) is isolated; for every n there are finitely many formulas in n free variables up to T-equivalence. Vaught's theorem: no complete theory in a countable language has exactly two countable models up to isomorphism. Examples: DLO has, over ∅, the types determined by the order relations among the variables, all isolated, S_n finite — DLO is ℵ_0-categorical; ACF_0 over a subfield k has, in one variable, the algebraic types (each isolated by a minimal polynomial) and the single non-isolated transcendental/generic type p_∞ saying x ≠ each element of the algebraic closure; (ℤ, +) and Th(ℕ, +, ·) have rich type spaces.
Chang, C. C. and Keisler, H. J. — Model Theory · Studies in Logic and the Foundations of Mathematics 73, 3rd edition, North-Holland (1990), Chapters 2-5. The systematic source for types and omitting types. Defines an n-type of a theory T as a set of formulas in n free variables consistent with T, complete when maximal; develops realization and omission in elementary extensions, and the type-space topology. Proves the Omitting Types Theorem by a Henkin construction with forcing of equality and existential witnesses: enumerate the sentences of an expanded language with countably many new constants c_0, c_1, ..., build a complete consistent Henkin theory T* ⊇ T step by step, and at the step handling the tuple of constants c̄ that might realize the non-isolated type p, use non-isolation to add a formula ¬θ(c̄) for some θ ∈ p consistent with the finite theory built so far (possible exactly because p is not isolated by the finite conjunction accumulated), so the term model of T* omits p. Presents the dual realizing constructions (saturated and special models realizing many types), the existence of countable saturated models for theories with countably many types over each finite set, and the back-and-forth uniqueness of countable saturated and of atomic/prime models. Establishes the Ryll-Nardzewski theorem and the analysis of countable models, including Vaught's theorem that the number of countable models is never exactly two.
Ryll-Nardzewski, C. — On the categoricity in power ≤ ℵ_0 · Bulletin de l'Académie Polonaise des Sciences, Série des sciences mathématiques, astronomiques et physiques 7 (1959), pp. 545-548. The characterization (obtained independently by Ryll-Nardzewski, Engeler, and Svenonius around 1959) of countable complete theories categorical in the countable power: a complete theory T with infinite models in a countable language is ℵ_0-categorical iff for each n there are only finitely many formulas in n free variables up to provable equivalence over T, equivalently iff the type space S_n(T) is finite for every n, equivalently iff every complete n-type over the empty set is isolated. The forward direction uses that a non-isolated type would be omittable (by the omitting types theorem) yet also realizable (in a saturated model), producing two non-isomorphic countable models; the reverse direction builds an isomorphism between any two countable models by back-and-forth, the finiteness of types making every tuple's type isolated hence preserved, so each structure is the unique countable atomic = saturated model.
Vaught, R. L. — Denumerable models of complete theories · In Infinitistic Methods (Proceedings of the Symposium on Foundations of Mathematics, Warsaw 1959), Pergamon and PWN (1961), pp. 303-321. Introduces the systematic theory of the countable models of a complete theory: the prime (atomic) model, the countable saturated model, and the spectrum I(T, ℵ_0) of countably many countable models. Proves that the prime model, when it exists, is the unique countable atomic model and embeds elementarily into every model, and that the countable saturated model, when it exists, is unique and universal among countable models; both are obtained by realizing, respectively omitting, families of types via the omitting types theorem. Proves Vaught's theorem that I(T, ℵ_0) ≠ 2 — no complete theory has exactly two countable models — by the argument that two models force a third: a theory with a non-isolated type has the prime model (omitting a maximal non-isolated type) distinct from a model realizing it, and a third model is constructed realizing some but not all such types. States Vaught's conjecture that I(T, ℵ_0) is either ≤ ℵ_0 or 2^{ℵ_0}, never strictly in between, which drives the descriptive-set-theoretic analysis of the type space.

Estimated time

beginner: 20m
intermediate: 54m
master: 90m