Let M be a structure for the language L. A partial type in a variable x is a set of L(M)-formulas in the free variable x, i.e., a set of formulas in the free variable x with parameters from M. Usually a type is denoted something like {\displaystyle \Sigma (x)}, and then {\displaystyle \Sigma (c)} denotes the set of sentences obtained by substituting c for x.

If x is a tuple of length n, a type in the variable x is called a partial n-type. When n isn't specified, the default may or may not be 1-types, depending on one's conventions.

A partial type is consistent if it is finitely satisfiable: for every finite subset {\displaystyle \Sigma _{0}(x)\subset \Sigma (x)}, there is a tuple cM such that

{\displaystyle M\models \phi (c)} for every {\displaystyle \phi (x)\in \Sigma _{0}(x)}.

If there is an element c which already satisfies all the formulas in {\displaystyle \Sigma (x)}, we say that c realizes {\displaystyle \Sigma (x)}, and that {\displaystyle \Sigma (x)} is realized in M.

One can think of a type as describing some kind of "ideal element" which may not actually exist in M. For example, in the structure (N,+,*,>), the partial 1-type {x > 0, x > 1, x > 2, ...} describes an "infinite" element. This type is not realized.

If A is a subset of M, a partial type over A is a set of L(A)-formulas in the free variable x, i.e., a partial type in which all the parameters come from A.

A complete type over A is a maximal consistent partial type over A. Complete types are often denoted with letters p, q. If p(x) is a complete type over A, then for every formula {\displaystyle \phi (x;a)} with aA, either

{\displaystyle \phi (x;a)\in p(x)} or {\displaystyle \neg \phi (x;a)\in p(x)}

and not both.

The unqualified term "type" may refer by default to partial types, or to complete types, depending on one's conventions. In Stability theory, the tendency is for "type" to mean complete type.

The type of an element[]

If b is a tuple from M and A is a subset of M, the type of b over A denoted tp(b/A), is the set of all formulas {\displaystyle \phi (x;a)} with aA and {\displaystyle M\models \phi (b;a)}. Then tp(b/A) is the unique complete type over A realized by b.

If b and c are two tuples from M of the same length, then it is customary to write

{\displaystyle b\equiv _{A}c}

to indicate that tp(b/A) = tp(c/A).

The space of complete types[]

The space of complete n-types over A is denoted Sn(A). This space is topologized by declaring the following set to be a basic open

{\displaystyle \{p(x)\in S_{n}(A):\phi (x)\in p(x)\}}

for each formula {\displaystyle \phi (x;a)} with aA.

With this topology, Sn(A) becomes a boolean space, that is, a totally disconnected compact topological space. This is called the Stone space of n-types over A. Under Stone duality, this space is dual to the boolean algebra of A-definable subsets of Mn

This comes from the relatively easy fact that a complete n-type over A is exactly the same thing as a homomorphism of boolean algebras from the boolean algebra of A-definable subsets of Mn to the two element boolean algebra {0,1}. This homomorphism sends a set of the form {\displaystyle \phi (M;a)} to 1 if {\displaystyle \phi (x;a)\in p(x)} and 0 otherwise.

Partial types over A essentially correspond to closed subsets of Sn(A). Under this correspondence, consistent types correspond to non-empty sets, complete types correspond to singletons, and finite types correspond to clopen subsets.

Restricting and Extending Types[]

If ABM, then any complete type p over B has a canonical restriction to a complete type over A, denoted p|A. This restriction type is characterized by the property that an A-formula {\displaystyle \phi (x;a)} is in p|A' if and only if it is in p.

This yields a map on Stone spaces Sn(B) -> Sn(A). This map is easily seen to be continuous.

It is also surjective: any complete type on A can be extended to a complete type on B. This follows from a more general fact: any consistent partial type on B can be extended to a complete type on B. The more general fact follows almost directly from Zorn's lemma.

Types in elementary extensions[]

Many properties of types behave well in elementary extensions. Specifically, suppose N is an elementary extension of M. Then

Moreover, it turns out that types can be realized in elementary extensions:

Theorem: Let M be a structure, and {\displaystyle \Sigma (x)} be a consistent partial type over M. Then there is an elementary extension {\displaystyle N\succeq M} and a tuple c from N such that c realizes {\displaystyle \Sigma (x)}.

Proof: Let T be the union of {\displaystyle \Sigma (c)} and the elementary diagram of M, where c is a new constant symbol not occurring in L(M). Any finite subset T0T has a model, namely M with the constant symbol c realizing the finite part of {\displaystyle \Sigma (x)} that appears in T0. Therefore, T has a model N by compactness. The structure N is an elementary extension of M because T contains the elementary diagram of M. Also, the interpretation of the constant c in N is a realization of {\displaystyle \Sigma (x)}. QED.

This fact gives an alternative description of complete types:

{\displaystyle S_{n}(A)=\{{\text{tp}}(a/A):a\in N^{n},~N\succeq M\}}

With a little bit more work, we can make an elementary extension in which all types over M are realized. Iterating this construction yields various kinds of saturated models.

Infinitary types[]

It makes sense to talk about types {\displaystyle \Sigma (x)} when the tuple x has infinite length. Note that a formula about x can only refer to finitely many coordinates from x, however. There is still a Stone space of types. If a is an infinite tuple from M, we can still talk about tp(a/A), and it makes sense to say that two infinite tuples (of the same length) have the same type over a subset of M. Essentially all of the above discussion carries through.

Global types[]

When working inside a monster model, most types that one considers are over small sets. To refer to types over the monster, the term global type is sometimes used. If working in a class-sized monster, there may be set-theoretic problems with the collection of all global types.

[Quantifier-free types, ∆-types, etc.]{#Quantifier-free_types,_∆-types,_etc. .mw-headline}[]

A quantifier-free type is a type containing only quantifier-free formulas. A complete quantifier-free type over A is a maximal consistent quantifier-free type over A, this will usually not be a complete type over A. Given an element a from M, one sometimes writes qftp(a/A) for the complete quantifier-free type over a over A.

The space of complete quantifier-free types has the usual Stone space topology. There is a natural restriction map from complete types over A to complete quantifier-free types over A. This map is continuous and surjective. It is a bijection if and only if every definable set over A is also quantifier-free definable.

In particular, the complete theory of M has quantifier elimination if and only if the map from complete n-types over {\displaystyle \emptyset } to complete quantifier-free n-types over {\displaystyle \emptyset } is a bijection.

When quantifier elimination holds, complete types are essentially the same thing as complete quantifier-free types.

Quantifier-free types have a nice interpretation in terms of substructures:

Fact: If M is a model, A is a subset of M, and a and b are two tuples from M of the same length, then

{\displaystyle {\text{qftp}}(a/A)={\text{qftp}}(b/A)}

if and only if the substructure generated by a and A is isomorphic to the substructure generated by b and A, by an isomorphism fixing A and sending a componentwise to b.

More generally, let {\displaystyle \Delta } be a set of formulas of the form {\displaystyle \phi (x;y)} with x a tuple of some fixed length. A ∆-formula over A is a boolean combination of formulas of the form {\displaystyle \phi (x;a)} with a from A and {\displaystyle \phi (x;y)\in \Delta }. A ∆-type over A is a type consisting of ∆-formulas and a complete ∆-type over A is a maximal consistent ∆-type over A. In the case where ∆ is the set of quantifier-free formulas, this recovers the notion of quantifier-free type. In the case where ∆ is a single formula {\displaystyle \{\phi (x;y)\}}, one speaks of {\displaystyle \phi }-types.

(In some settings, one uses a slightly different definition of ∆-formula. For example, in Geometric Stability Theory, Pillay defines a ∆-formula over A to be a formula over A which is equivalent to a ∆-formula over some possibly larger set of parameters.)


Dense Linear Orders[]

The theory of Dense Linear Orders has quantifier-elimination, so complete types are the same thing as complete quantifier-free types. If M is a model of DLO, S is a subset, and a and b are two elements of M, then tp(a/S) = tp(b/S) if and only if

{\displaystyle \{s\in S:s>a\}=\{s\in S:s>b\}}


{\displaystyle \{s\in S:s<a\}=\{s\in S:s<b\}}.

In other words, two elements of M have the same type over S if and only if they induce the same Dedekind cut of S. Moreover, if M is sufficiently saturated, then every Dedekind cut of S will be inhabited.

Consequently, a complete 1-type over S is the same thing as a Dedekind cut over S. That is, to specify a complete 1-type p(x) over S, we just need to specify which elements of S are bigger than x and which are smaller.

More generally, to specify a complete n-type p(x1,...,xn) over a set SM, we must specify how each xi compares to each element of S, and additionally, how xi compares to xj for ij.

Algebraically Closed Fields[]

In the theory of Algebraically Closed Fields, types are closely connected to irreducible varieties:

Theorem: Let M be a model of ACF, and KM be a subfield. Let V be a closed subvariety of affine n-space, with V definable over K and irreducible as a K-variety (but not necessarily geometrically irreducible). Then there is a unique complete n-type p(x) over K which is characterized by the fact that a realization of p(x) lives on V, and not on any closed proper subvarieties of V defined over K. This is called the generic type of V.

Moreover, the map assigning to an irreducible variety the corresponding generic type yields a bijection between irreducible K-subvarieties of affine n-space and complete n-types over K.

(Equivalently, complete n-types over K correspond to scheme-theoretic points of {\displaystyle \mathbb {A} _{K}^{n}} := Spec K[X1,...Xn]), affine n-space over K.)

Proof: Let V be a K-irreducible closed subvariety of affine n-space. Let S be the set of strictly smaller closed K-subvarieties of affine n-space. Let p(x) be the n-type over K asserting that xV and xW for WS. We claim that this type is consistent and implies a complete type over K.

If p(x) is inconsistent, then there would exist a finite subset

{\displaystyle S_{0}=\{W_{1},\ldots ,W_{n}\}\subset S}

such that no x in Mn realized

{\displaystyle x\in V\wedge x\notin W_{1}\wedge \cdots x\notin W_{n}}

This would imply that

{\displaystyle V\subset W_{1}\cup \cdots \cup W_{n}}

But since each Wi is a proper closed subvariety of V, this would contradict irreducibility of V.

Consequently, p(x) is consistent, and can thus be extended to at least one complete type over K. If there were more than one complete type extending p(x), then passing to an elementary extension in which both types are realized, we could find two n-tuples a and b both satisfying p(x), having different types over K. If W is any closed K-subvariety of affine space, then either


Either way, we see that aWbW. Now if D is any K-definable set, then by quantifier elimination in ACF, D is a boolean combination of closed K-subvarieties of affine space. Since each contains a if and only if it contains b, the same is true of D. In particular, we cannot find a K-definable set D which contains a but not b, or vice versa. Consequently, a and b have the same type over K, a contradiction.

Therefore, p(x) implies a unique complete type over K. So every irreducible K-variety has a unique generic type.

Now let p(x) be an arbitrary complete n-type over K. Passing to an elementary extension, we may assume that p(x) is realized by an element a.

Claim: There is a minimum closed K-subvariety of affine n-space containing a. It is K-irreducible.

Proof: By Noetherianity of K[X1,...Xn] any descending chain of closed varieties must stabilize. Therefore, by Zorn's lemma, there is a minimal closed K-subvariety V containing a. If W is any closed K-subvariety containing a, then WV is another. By minimality of V, we must have VW. Therefore V is the unique smallest K-subvariety containing a.

If V were not K-irreducible, we could write V as a union V1V2 of two strictly smaller closed subvarieties. Then one of V1 or V2 would contain a, contradicting minimality of V. QEDclaim.

As a is on V, but not on any strictly smaller closed K-subvarieties, a realizes the generic type of V. So p = tp(a/K) is exactly the generic type of V.

So every complete n-type over K is the generic type of some irreducible variety. Moreover, this variety is unique: if V and W are two distinct K-irreducible varieties, then the generic type of V asserts that x is in V \ W, while the generic type of W asserts that x is in W \ V. These are contradictory, so V and W do not have the same generic type.


For example, 1-types over K correspond to K-irreducible subvarieties of the affine line. These are of two types:

The type corresponding to the entire line is the type of a transcendental over K. This type asserts that x is not algebraic over K.

The other types are the algebraic types over K. Each one asserts that x is algebraic over K, with some specific minimal polynomial. For example, if K is the rationals Q, then the type associated to X2 - 2 is the type of {\displaystyle \pm {\sqrt {2}}} over Q, while the type associated to X - 7 is the type of seven over Q.

Some motivation for Stability Theory[]

In light of the Theorem characterizing types in ACF, one can view the notion of "type" as a generalization of the notion of "irreducible variety." However, there are many basic operations on varieties which do not readily generalize to types. For example, if V and W are two irreducible varieties over K, then {\displaystyle V\times W} is (usually) an irreducible variety over K as well. Can we describe the generic type of {\displaystyle V\times W} in terms of the generic type of V and the generic type of W? In a general setting of model theory, there is no way to do this. However, in stable theories, there is a canonical way to take the tensor product of two types, which correctly corresponds to multiplying varieties.

On an even more basic level, if V is an irreducible variety over K, and L is a field extending K, then V is (usually) an irreducible variety over L as well. If this holds, then the generic type of V over K has a canonical extension to a type over L. Can this be generalized to arbitrary theories? Not really, it turns out. But again, in the special setting of stable theories, there is a canonical way to extend types, the notion of non-forking extensions. Then one can say that the generic type of V over L is the unique non-forking extension to L of the generic type of V over K.

Moreover, many concepts from stability theory generalize concepts from algebraic geometry via the example of ACF. For example, Morley rank, Lascar rank and other ranks generalize dimension. Non-forking independence generalizes algebraic independence. Stationarity generalizes geometric irreducibility.

One can also see from our two examples (ACF and DLO) the difference in number of types between a stable theory (ACF) and an unstable theory (DLO). If K is a subfield of a model of ACF, then the number of complete n-types over K is the same as the number of irreducible K-varieties in affine n-space, or equivalently, the number of prime ideals in K[X1,...Xn]. Since this ring is Noetherian, each prime ideal is finitely generated. By basic cardinal arithmetic, there end up being only about {\displaystyle |K|+\aleph _{0}} such ideals. Consequently, over any set K there end up being not many more types over K than the cardinality of K-itself. Thus ACF is {\displaystyle \kappa }-stable for all {\displaystyle \kappa }.

On the other hand, consider the rationals Q as a model of DLO. To specify a 1-type over Q, we must specify a Dedekind cut (roughly). So there are at least a continuum's worth of 1-types over Q. In particular, the number of types over Q exceeds the cardinality of Q. So DLO is not {\displaystyle \aleph _{0}}-stable. Replacing Q with appropriately chosen bigger total orders, one can prove that DLO is not {\displaystyle \kappa }-stable for any {\displaystyle \kappa }, so DLO is unstable. ::: ::: :::