type (in model theory)


Warning on terminology: This is a different notion than that of type in type theory, which is what model theorists call sorts.


The syntactic category of a Boolean coherent theory has a Boolean algebra structure on each of its subobject posets. Types are ultrafilters of the Boolean algebras of subobjects of the maximal objects in these syntactic categories (those corresponding to formulas of the form “x=xx=x”).

If one tries to add a global point to such a syntactic category (i.e. name a constant) “without changing anything”, this point must have a sort (in the sense of type from type theory), and hence must pick out a principal ultrafilter of definable sets which live above it in the subobject lattice. Types tell you what kinds of global points you can add. When you have “all possible” such global points plus a homogeneity condition, you’re in a saturated monster model.


Let MM be a model (in Set\mathbf{Set}) of a first-order theory. Let m¯=(m 1,,m n) \overline{m} = (m_1, \dots, m_n) be a tuple of elements from that model. The type of m¯\overline{m} is the ultrafilter of definable sets of the same sort (type in the sense of type theory, sort in the sense of Makkai’s FOLDS) as m¯\overline{m} containing m¯\overline{m}.

Syntactically, if xx is a tuple of variables, an xx-type is a finitely consistent (hence consistent, by the compactness theorem) set of formulas whose tuple of free variables has the same sort (arity) as ss. These correspond to filters of definable sets. A type corresponds to an ultrafilter of definable sets if and only if it is a maximally consistent set of formulas; we call such a type complete.

By Stone duality, the set of all complete xx-types of a theory TT inherits a Stone topology, and is called the Stone space S x(T)S_x(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 is related to the study of types, and the phenomenon of forking in model theory; that aspect is studied in stability theory.

Saturation and the monster model

If mm is a tuple of sort ss, and pp is an ss-type, we say that mm realizes the type pp if the type of mm is pp.

By the completeness theorem, we can always realize types in larger elementary extensions if they aren’t already realized in your model. For example, this is how one usually obtains a nonstandard model of arithmetic, because one can form the type (with parameters coming from the \mathbb{N}, which is small) which says “any realization of this must not equal anything in \mathbb{N}.”

More generally, let AA be a subset of the model MM. If we also allow parameters from AA in our formulas, we can form types over AA. We say that a model is κ\kappa-saturated if all types over AA for |A|=κ|A| = \kappa are realized.

Saturated models always exist (maybe modulo some large cardinal assumptions.) For example, an 0\aleph_0-saturated elementary extension of the natural numbers (,)(\mathbb{N}, \leq) equipped with their usual ordering just looks like \mathbb{N} with ω\omega-many copies of (,)(\mathbb{Z}, \leq) stacked on top, each of them comprising points at infinity.

In modern model theory it is customary to work in a Grothendieck universe-sized or class-sized monster model, so that all types over small parameter sets are realized. Inside a monster 𝕄\mathbb{M} things often get more explicitly geometric. For example, two tuples aa and bb in 𝕄\mathbb{M} will have the same type if and only if they are Aut(𝕄)\operatorname{Aut}(\mathbb{M})-conjugate, i.e. lie in the same orbit of the automorphism group of the monster, and in the presence of two constants the syntactic category is Barr-exact (i.e. eliminates imaginary elements) if and only if all definable sets can be coded: for all XSyn(T),X \in \mathsf{Syn}(T), there exists a tuple xx such that any automorphism which fixes XX setwise fixes xx pointwise.

Stated in this form, it’s easy to see that the theory of algebraically closed fields codes at least all finite parameter sets. This paves the way for model-theoretic Galois theory.


  • In the theory of an equivalence relation with two infinite classes, the type (over the empty set) of a point in any model is isolated in the Stone space by the formula which says which equivalence class that point belongs to.

Types generalize points by replacing them with their principal ultrafilters of definable sets. 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.

Relation to measures


  • 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)
  • Lou van den Dries, An Introduction To Model-Theoretic Stability, online notes

Revised on September 5, 2016 13:49:15 by jesse (