type (in model theory)


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


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

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

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

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 MM a larger model MM'. 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 MM'. 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 (