structural:scholar_edition, information:highlighting, linguistic:translation, information:extraction
Formal definition

Consider a structure M {\displaystyle {\mathcal {M}}} for a language L. Let M be the universe of the structure. For every A ⊆ M, let L (A) be the language obtained from L by adding a constant c for every a ∈ A. In other words,

A 1-type (of M {\displaystyle {\mathcal {M}}}) over A is a set p (x) of formulas in L (A) with at most one free variable x (therefore 1-type) such that for every finite subset p (x) ⊆ p (x) there is some b ∈ M, depending on p (x), with M ⊨ p 0 (b) {\displaystyle {\mathcal {M}}\models p_{0}(b)} (i.e. all formulas in p (x) are true in M {\displaystyle {\mathcal {M}}} when x is replaced by b).

Similarly an n -type (of M {\displaystyle {\mathcal {M}}}) over A is defined to be a set p (x,..., x) = p (x) of formulas in L (A), each having its free variables occurring only among the given n free variables x,..., x, such that for every finite subset p (x) ⊆ p (x) there are some elements b,..., b ∈ M with M ⊨ p 0 (b 1, …, b n) {\displaystyle {\mathcal {M}}\models p_{0}(b_{1},\ldots,b_{n})}.

A complete type of M {\displaystyle {\mathcal {M}}} over A is one that is maximal with respect to inclusion. Equivalently, for every ϕ (x) ∈ L (A, x) {\displaystyle \phi ({\boldsymbol {x}})\in L(A,{\boldsymbol {x}})} either ϕ (x) ∈ p (x) {\displaystyle \phi ({\boldsymbol {x}})\in p({\boldsymbol {x}})} or ¬ ϕ (x) ∈ p (x) {\displaystyle \lnot \phi ({\boldsymbol {x}})\in p({\boldsymbol {x}})}. Any non-complete type is called a partial type. So, the word type in general refers to any n -type, partial or complete, over any chosen set of parameters (possibly the empty set).

An n -type p (x) is said to be realized in M {\displaystyle {\mathcal {M}}} if there is an element b ∈ M such that M ⊨ p (b) {\displaystyle {\mathcal {M}}\models p({\boldsymbol {b}})}. The existence of such a realization is guaranteed for any type by the compactness theorem, although the realization might take place in some elementary extension of M {\displaystyle {\mathcal {M}}}, rather than in M {\displaystyle {\mathcal {M}}} itself. If a complete type is realized by b in M {\displaystyle {\mathcal {M}}}, then the type is typically denoted t p n M (b / A) {\displaystyle tp_{n}^{\mathcal {M}}({\boldsymbol {b}}/A)} and referred to as the complete type of b over A.

A type p (x) is said to be isolated by φ {\displaystyle \varphi }, for φ ∈ p (x) {\displaystyle \varphi \in p(x)}, if for all ψ (x) ∈ p (x), {\displaystyle \psi ({\boldsymbol {x}})\in p({\boldsymbol {x}}),} we have Th (M) ⊨ φ (x) → ψ (x) {\displaystyle \operatorname {Th} ({\mathcal {M}})\models \varphi ({\boldsymbol {x}})\rightarrow \psi ({\boldsymbol {x}})}. Since finite subsets of a type are always realized in M {\displaystyle {\mathcal {M}}}, there is always an element b ∈ M such that φ (b) is true in M {\displaystyle {\mathcal {M}}}; i.e. M ⊨ φ (b) {\displaystyle {\mathcal {M}}\models \varphi ({\boldsymbol {b}})}, thus b realizes the entire isolated type. So isolated types will be realized in every elementary substructure or extension. Because of this, isolated types can never be omitted (see below).

A model that realizes the maximum possible variety of types is called a saturated model, and the ultrapower construction provides one way of producing saturated models.