Type (model theory)

From Wikipedia, the free encyclopedia

The introduction to this article provides insufficient context for those unfamiliar with the subject.
Please help improve the article with a good introductory style.

In model theory, consider a structure of signature σ, $M$ , a set of parameters $A \subset M$ and some tuple of elements of $M$ , $\bar{b} \in M^n$ .

The complete type of $\bar{b}$ over $A$ is the set of all first-order σ-formulae $ψ$ with free variables $x_1,x_2,\ldots,x_n$ , and parameters in $A$ which are satisfied by $\bar{b}$ .

For example, the complete type of the number 2 over the emptyset, 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 1+1+1$ , $x\le 1+1+1+1+1$ , and $\exists y(y<x)$ .

By definition the complete type of an element is a consistent set of formulae, and is maximal, i.e. for all formulae $\psi(x_1,\ldots,x_n)$ with parameters in $A$ , either $ψ$ is in the type or $\lnot \psi$ is in the type.

A complete $n$ -type over $A$ is, therefore, defined to be any maximal consistent set of formulae with parameters in $A$ and free variables $x_1,\ldots,x_n$ . Note that a complete $n$ -type $p$ may be the complete type of some $\bar{b} \in M^n$ ; we then say that $\bar{b}$ realises $p$ . This is not necessarily the case. However, given any complete $n$ -type $p$ over $A$ , there is some elementary superstructure $N$ of $M$ and an element $\bar{c} \in N^n$ so that $\bar{c}$ realises $p$ , in other words $p$ is the complete type of $c$ over $A$ .

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 partial $n$ -type over $A$ is any consistent (but not necessarily maximal) set of formulae with parameters in $A$ and free variables $x_1,\ldots,x_n$ . Any complete type is a partial type. Conversely, it can be proved that, any partial type is a subset of a complete type. The word type is sometimes used to mean complete type and sometimes any partial type.

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 cannot. For example, using the entire set of real numbers as constants one 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

It is useful to consider the set of complete $n$ -types over $A$ as a topological space. Consider the following equivalence relation on formulae in the free variables $x_1,\ldots,x_n$ with parameters in $M$ : $\psi \equiv \phi$ iff $M \models \forall x_1,\ldots,x_n (\psi(x_1,\ldots,x_n) \leftrightarrow \phi(x_1,\ldots,x_n))$ . One can show that $\psi \equiv \phi$ iff they are contained in exactly the same complete types.

The set of formulae in free variables $x_1,\ldots,x_n$ over $A$ up to this equivalence relation is a Boolean algebra (and is canonically isomorphic to the set of $A$ -definable subsets of $M n$ ). The complete n-types correspond 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. The complete theory of algebraically closed fields of characteristic 0 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.

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 corrresponding to p is the set of polynomials 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.

[edit] The omitting types theorem

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 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 algebraically 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.