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

Idea

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

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.

More heuristics

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.

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 September 21, 2012 00:06:51
by Urs Schreiber
(82.169.65.155)