Complete type

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

A complete two-type is a complete type in two free variables. Such a partial type describes both individual properties and relations between a pair of elements.

A complete one-type is a complete type in one free variable. It chooses exactly one of each first-order formula and its negation consistently with the first-order theory and the named parameters.

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 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 every subset of the standard prime numbers, prescribe exactly which of those primes divide a nonzero element. Every finite prescription is realized by the product of its finitely many positive divisibility requirements. Compactness theorem extends each prescription to a complete one-type of the complete theory of the integer ring. Different subsets give incompatible partial types. The countable first-order language supplies the matching upper bound.

For each irrational real cut $r$, the displayed comparisons with named rationals are finitely satisfiable. Quantifier elimination for dense linear orders makes them determine a complete type, omitted by the named rational structure itself. Different cuts give different types, so there are continuum many. An omega-saturated model must realize all of them and cannot be countable, although the named rational structure is countable, atomic and prime.

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

A principal complete type is isolated by one first-order consistent first-order formula: modulo the first-order theory, that logical formula implies every member of the partial type. For complete types this is exactly an isolated type. The qualifier complete distinguishes this notion from partial types.

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.