type (in model theory)

**Warning** on terminology: This is unrelated to the notion of *type* in type theory.

In model theory, an $n$-type is a set of first order formulas $p(x_1,\ldots,x_n)$ in a language $L$ with $n$ free variables $x_1,\ldots,x_n$, which are true for some sequence of $n$-elements of an $L$-structure $M$ substituted for $x_1,\ldots,x_n$. One often limits consideration to the models $M$ of a given $L$-theory $T$.

A type is said to be *complete* if it is a maximally consistent set of $L$-formulas.

Complete types correspond to ultrafilters of definable sets. By Stone duality, the set of all $n$-types of a theory $T$ inherits a Stone topology, and is called the *Stone space* $S_n(T)$ of the theory $T$.

There are some extension of this notion of type beyond first order, for example the notion of Galois types in infinitary logic, which is particularly important i the study of abstract elementary classes.

An important method toward classification of theories is study of the number of nonisomorphic models in each cardinality; its study if related to the study of types, and the phenomenon of forking in model theory; that aspect is studied in stability theory.

The simplest first order theories are generalizations of algebraic geometry where points correspond to special (e.g. maximal, prime) ideals in a ring; types generalize points in some of such cases. Other “spectral” intuition also applies.

Finally, one may expand the model $M$ a larger model $M'$. The elements of automorphism group of the larger model will move the “points” around and a type will become an orbit for the larger model $M'$. This point of view is used especially for the generalization, so called Galois types.

- Wikipedia,
*type (model theory)*, forking extension - Siu-Ah Ng,
*Forking*, (Springer Online) Encyclopedia of Mathematics. web (note inside the wrong link (cross reference) to a type in the sense of type theory)

Revised on April 9, 2016 02:41:19
by Anonymous Coward
(66.205.168.251)