Type (model theory)

In model theory and related areas of mathematics, a type is an object that, loosely speaking, describes how a (real or possible) element or elements in a mathematical structure might behave. More precisely, it is a set of first-order formulas in a language L with free variables x1, x2,…, xn that are true of a sequence of elements of an L-structure M {displaystyle {mathcal {M}}} . Depending on the context, types can be complete or partial and they may use a fixed set of constants, A, from the structure M {displaystyle {mathcal {M}}} . The question of which types represent actual elements of M {displaystyle {mathcal {M}}} leads to the ideas of saturated models and omitting types. In model theory and related areas of mathematics, a type is an object that, loosely speaking, describes how a (real or possible) element or elements in a mathematical structure might behave. More precisely, it is a set of first-order formulas in a language L with free variables x1, x2,…, xn that are true of a sequence of elements of an L-structure M {displaystyle {mathcal {M}}} . Depending on the context, types can be complete or partial and they may use a fixed set of constants, A, from the structure M {displaystyle {mathcal {M}}} . The question of which types represent actual elements of M {displaystyle {mathcal {M}}} leads to the ideas of saturated models and omitting types. 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 ca 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 p0(x) ⊆ p(x) there is some b ∈ M, depending on p0(x), with M ⊨ p 0 ( b ) {displaystyle {mathcal {M}}models p_{0}(b)} (i.e. all formulas in p0(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(x1,…,xn) = p(x) of formulas in L(A), each having its free variables occurring only among the given n free variables x1,…,xn, such that for every finite subset p0(x) ⊆ p(x) there are some elements b1,…,bn ∈ M with M ⊨ p 0 ( b 1 , … , b n ) {displaystyle {mathcal {M}}models p_{0}(b_{1},ldots ,b_{n})} . Complete type refers to those types that are maximal with respect to inclusion, i.e. if p(x) is a complete type, then for every ϕ ( x ) ∈ L ( A , x ) {displaystyle phi ({oldsymbol {x}})in L(A,{oldsymbol {x}})} either ϕ ( x ) ∈ p ( x ) {displaystyle phi ({oldsymbol {x}})in p({oldsymbol {x}})} or ¬ ϕ ( x ) ∈ p ( x ) {displaystyle lnot phi ({oldsymbol {x}})in p({oldsymbol {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 ∈ Mn such that M ⊨ p ( b ) {displaystyle {mathcal {M}}models p({oldsymbol {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}}({oldsymbol {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 ∀ ψ ( x ) ∈ p ( x ) , φ ( x ) → ψ ( x ) {displaystyle forall psi ({oldsymbol {x}})in p({oldsymbol {x}}),varphi ({oldsymbol {x}}) ightarrow psi ({oldsymbol {x}})} . Since finite subsets of a type are always realized in M {displaystyle {mathcal {M}}} , there is always an element b ∈ Mn such that φ(b) is true in M {displaystyle {mathcal {M}}} ; i.e. M ⊨ φ ( b ) {displaystyle {mathcal {M}}models varphi ({oldsymbol {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. Consider the language with one binary connective, which we denote as ∈ {displaystyle in } . Let M {displaystyle {mathcal {M}}} be the structure ⟨ ω , ∈ ω ⟩ {displaystyle langle omega ,in _{omega } angle } for this language, which is the ordinal ω {displaystyle omega } with its standard well-ordering. Let T {displaystyle {mathcal {T}}} denote the theory of M {displaystyle {mathcal {M}}} .