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 “”).
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, you’re in a saturated monster model.
Let be a model (in ) of a first-order theory. Let be a tuple of elements from that model. The type of 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 containing .
Syntactically, if is a tuple of variables, an -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 . 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 -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 is related to the study of types, and the phenomenon of forking in model theory; that aspect is studied in stability theory.
If is a tuple of sort , and is an -type, we say that realizes the type if the type of is .
By the completeness theorem, we can always realize types in larger models. For example, this is how one usually obtains a nonstandard model of arithmetic.
Let be a subset of the model . If we also allow parameters from in our formulas, we can form types over . We say that a model is -saturated if all types over for are realized.
Saturated models always exist (maybe modulo some large cardinal assumptions.) For example, an -saturated elementary extension of the natural numbers equipped with their usual ordering just looks like with -many copies of stacked on top, each of them containing 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 things often get more explicitly geometric. For example, two tuples and in will have the same type if and only if they are -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-effective (i.e. eliminates imaginary elements) if and only if all definable sets can be coded: for all there exists a tuple such that any automorphism which fixes setwise fixes 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?.
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.