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.
For every A ⊆ M, let L(A) be the language obtained from L by adding a constant ca for every a ∈ A.
) 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
) 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
So, the word type in general refers to any n-type, partial or complete, over any chosen set of parameters (possibly the empty set).
So isolated types will be realized in every elementary substructure or extension.
Consider the language L with one binary relation symbol, which we denote as
Well, we can just take the successor of the largest ordinal mentioned in the set of formulas
If we wanted to realize the type, we might be tempted to consider the structure
Another example: the complete type of the number 2 over the empty set, considered as a member of the natural numbers, would be the set of all first-order statements (in the language of Peano arithmetic), describing a variable x, that are true when x = 2.
This is an example of an isolated type, since, working over the theory of the naturals, the formula
As a further example, the statements and describing the square root of 2 are consistent with the axioms of ordered fields, and can be extended to a complete type.
Similarly, the infinite set of formulas (over the empty set) {x>1, x>1+1, x>1+1+1, ...} is not realized in the ordered field of real numbers, but is realized in the ordered field of hyperreals.
that is realized by an infinitesimal hyperreal that violates the Archimedean property.
The reason it is useful to restrict the parameters to a certain subset of the model is that it helps to distinguish the types that can be satisfied from those that cannot.
It is useful to consider the set of complete n-types over A as a topological space.
Consider the following equivalence relation on formulas in the free variables x1,..., xn with parameters in A: One can show that
The set of formulas in free variables x1,...,xn over A up to this equivalence relation is a Boolean algebra (and is canonically isomorphic to the set of A-definable subsets of Mn).
The complete n-types correspond to ultrafilters of this Boolean algebra.
The complete theory of algebraically closed fields of characteristic 0 has quantifier elimination, which allows one to show that the possible complete 1-types (over the empty set) correspond to: In other words, the 1-types correspond exactly to the prime ideals of the polynomial ring Q[x] over the rationals Q: if r is an element of the model of type p, then the ideal corresponding to p is the set of polynomials with r as a root (which is only the zero polynomial if r is transcendental).
More generally, the complete n-types correspond to the prime ideals of the polynomial ring Q[x1,...,xn], in other words to the points of the prime spectrum of this ring.
(The Stone space topology can in fact be viewed as the Zariski topology of a Boolean ring induced in a natural way from the Boolean algebra.
While the Zariski topology is not in general Hausdorff, it is in the case of Boolean rings.)
For example, if q(x,y) is an irreducible polynomial in two variables, there is a 2-type whose realizations are (informally) pairs (x,y) of elements with q(x,y)=0.
Given a complete n-type p one can ask if there is a model of the theory that omits p, in other words there is no n-tuple in the model that realizes p. If p is an isolated point in the Stone space, i.e. if {p} is an open set, it is easy to see that every model realizes p (at least if the theory is complete).
The field of algebraic numbers is a model omitting this type, and the algebraic closure of any transcendental extension of the rationals is a model realizing this type.