Type (model theory)

From Wikipedia, the free encyclopedia

You have new messages (last change).

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<x). Note: Some authors prefer to use the words "partial type" and "type", in place of "type" and "complete type" respectively.

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<x)

and

\forall y((y>0 \and 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 {x>1, x>1+1, x>1+1+1, ...} 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 < y + 7 would occur in a type defined over two variables, x and y, and over a set of constants that included the number 7. The reason it is useful to restrict the constants to a certain subset of the model is that it helps to distinguish the types that can be satisfied from those that can't. For example, if we were allowed to use the entire set of real numbers as constants, then we could generate an uncountably infinite list of formulae like x\ne 1, x\ne \pi, ... that would explicitly rule out every possible real value for x, and therefore could never be realized within the real numbers.

[edit] 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 formulas in n variables is a boolean algebra, and the complete n-types correspend to ultrafilters of this boolean algebra. 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. This constructs the Stone space which is compact, Hausdorff, and totally disconnected.

Example. Suppose that the theory is the complete theory of algebraically closed fields of characteristic 0. This theory has quantifier elimination which allows one to show that 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[x1,...,x1], 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.

[edit] 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.

[edit] References

Retrieved from "http://en.wikipedia.org../../../t/y/p/Type_%28model_theory%29.html"