nLab
type (in model theory)

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,\dots ,x_n)$ in a language $L$ with $n$ free variables $x_1,\dots ,x_n$, which are true for some sequence of $n$-elements of an $L$-structure $M$ substituted for $x_1,\dots ,x_n$. One often limits consideration to the models $M$ of a given $L$-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.

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\prime$. 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\prime$. This point of view is used especially for the generalization, so called Galois types.

Related concepts

• topos of types
• forking
• Galois type
• stability theory

References

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