Type (model theory)

In model theory and related areas of mathematics, a type is an object that describes how a (real or possible) element or finite collection of 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 set of n-tuples of an L-structure . Depending on the context, types can be complete or partial and they may use a fixed set of constants, A, from the structure . The question of which types represent actual elements of leads to the ideas of saturated models and omitting types. Consider a structure 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 ) 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 (i.e. all formulas in p0(x) are true in when x is replaced by b). Similarly an n-type (of ) 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 . A complete type of over A is one that is maximal with respect to inclusion. Equivalently, for every either or . 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 if there is an element b ∈ Mn such that . 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 , rather than in itself. If a complete type is realized by b in , then the type is typically denoted and referred to as the complete type of b over A.