Complete type

The complete type of a tuple over parameters records every formula over those parameters that the tuple satisfies.

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.

With its standard topology, this type space is a Stone space. The type space $S_n^M(A)$ is the set of complete $n$-types over a parameter set $A$ that are consistent with the complete theory of $M$ together with its diagram over $A$.

For a type space $S_n^M(A)$, the basic open set $[\phi ]$ consists of complete types containing the formula $\phi$. These sets are clopen, satisfy $[\phi ]\cap [\psi ]=[\phi \wedge \psi ]$, and distinguish distinct types. The compactness theorem makes this topology compact; it is Hausdorff and has a basis of clopen sets.

A complete type $p\in S_n(A)$ is isolated when some formula $\phi \in p$ belongs to no other complete type in $S_n(A)$. Equivalently, the basic open set determined by $\phi$ is the singleton $\{p\}$.

If a complete countable theory has a prime model, isolated types are dense in every finite-arity type space. Every nonempty basic open set is realized in the prime model, whose finite tuples have isolated types.

A type $p(x_1,\dots ,x_n)$ is omitted in a structure $M$ when no tuple from $M^n$ realizes every formula in $p$.

Let $T$ be a consistent theory in a countable first-order language. For every countable family of nonisolated finite-arity types of $T$, there is a countable model of $T$ that omits every type in the family.

Let $p(\mathbf{x})$ be a nonprincipal partial type over a consistent first-order theory $T$. Suppose $T\cup \{\sigma (\mathbf{c})\}$ is consistent, with $\sigma$ a finite condition in finitely many new constants, and let $\mathbf{t}(\mathbf{c})$ be a tuple of closed terms. Some $\psi \in p$ leaves $T\cup \{\sigma (\mathbf{c}),\neg \psi (\mathbf{t}(\mathbf{c}))\}$ consistent. Otherwise the original-language first-order formulais consistent with $T$ and entails every member of $p$, contradicting nonprincipality. Replace all new constants occurring in the condition or terms by variables. This lemma makes the omission requirements dense in a countable Henkin construction.

Every complete type over parameters from $M$ is realized in some elementary extension of $M$. Apply compactness to the elementary diagram of $M$ together with a new tuple of constants satisfying the type.

Distinct complete types contain opposite choices $\phi$ and $\neg \phi$. The corresponding basic clopen sets partition the type space, so every type space is totally disconnected.

Quantifier elimination for dense linear orders shows that the one-types over $\mathbb{N}\subset \mathbb{Q}$ are determined by cuts: equality to a natural number, one of the intervals between consecutive natural numbers, the ray below zero, or the cut above every natural number. Only the last type is non-isolated.

A model is aleph-zero-homogeneous when every finite partial elementary map extends by one more element.