= Solution
A complete $n$-type over $T$ is a maximal <set> $p(\bar x)$ of formulas in $n$ variables <consistent first-order theory>[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 first-order theory>[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 first-order theory>[consistent] <first-order theory>[theory] has a <countable> <first-order model>[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 <first-order model>[model] realizes all formulas of the type, even though each finite <subset> is compatible with the <first-order theory>[theory].
Back to article page
