In model theory, an -type is a set of first order formulas in a language with free variables , which are true for some sequence of -elements of an -structure substituted for . One often limits consideration to the models of a given -theory .
A type is said to be complete if it is a maximally consistent set of -formulas.
Complete types correspond to ultrafilters of definable sets. By Stone duality, the set of all -types of a theory inherits a Stone topology, and is called the Stone space of the theory .
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 a larger model . 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 . This point of view is used especially for the generalization, so called Galois types.