Type (model theory)

Encyclopedia : T : TY : TYP : Type (model theory)

In model theory, a type is a set of formulae in first-order logic such that all the formulae could be consistent descriptions of a certain element (or several elements) of the model. A complete type is a maximal such set (that is, for every first-order question about the elements, the type answers either "yes" or "no"). For example, the complete type of the number 2, considered as a member of the natural numbers, would be the list of all first-order statements describing a variable x that are true for x=2. This list would include statements such as [x\ne 3], [x\le 5], and [\exists y(y Some types may not be realized within a particular model, but may be realizable in an extension of that model. For example, the statements

[\forall y(y^2<2 \implies y

and

[\forall y(y^2>2 \implies y>x)]

describing the square root of 2 are consistent with each other and with the axioms of arithmetic, and can be extended to form a complete type. This type is not realized in the model of arithmetic consisting of the rational numbers, but is realized in the reals. Similarly, the infinite set of statements is not realized in the real numbers, but is realized in the hyperreals. 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.

A type typically is defined for formulae using a fixed number of free variables, and constants coming from a fixed subset of the model. For example, the formula [x

Stone spaces

We can also define complete n-types for an integer n; these are given by maximally consistent sets of formulas in n variables, so a 1-type is the same as a type. The set of complete n-types can be made into a topological space by taking the types containing a given formula as basic open sets. These spaces are Stone spaces, and are compact, Hausdorff, and totally disconnected.

Example. Suppose that the theory is the complete theory of algebraically closed fields of characteristic 0. The possible complete 1-types correspond to:

Roots of a given irreducible non-constant polynomial over the rationals with leading coefficient 1. For example, the type of square roots of 2. Each of these types is an open point of the Stone space.
Transcendental elements, that are not roots of any non-zero polynomial. This type is a point in the Stone space that is closed but not open.

Another way to describe this is to say that 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 corrresponding to p is the set of poynomials with r as a root. More generally, the complete n-types correspond to the prime ideals of the polynomial ring Q[x₁,...,x₁], in other words to the points of the prime spectrum of this ring. (But the Stone space topology is not the Zariski topology, which is not Hausdorff.) For example, if q(x,y) is an irreducible polynomial in 2 variables, there is a 2-type whose elements are (informally) pairs (x,y) of transcendental elements with q(x,y)=0.

The omitting types theorem

Suppose we have a complete n type p. We can ask if there is a model of the theory that omits p, in other words there is no n-tuple of type p. If p is isolated in the Stone space, in other words if it is an open point, it is easy to see that every model realizes p (at least if the theory is complete). The omitting types theorem says that conversely if p is not isolated then there is a countable model omitting p (provided that the language is countable).

Example: In the theory of algbraically closed fields of characteristic 0, there is a 1-type represented by elements that are transcendental over the prime field. This is a non-isolated point of the Stone space (in fact, the only non-isolated point). 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.

All the other types are "algebraic numbers" (more precisely, they are the sets of first order statements satisfied by some given algebraic number), and all such types are realized in all algebraically closed fields of characteristic 0.

References

Wilfrid Hodges, A shorter model theory (1997) Cambridge University Press ISBN 0-521-58713-1
C. C. Chang, H. J. Keisler Model theory ISBN 0720406927
David Marker Model Theory: An Introduction ISBN 0387987606