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 $\Sigma (x)$ , and then $\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 $\Sigma _{0}(x)\subset \Sigma (x)$ , there is a tuple c ∈ M such that

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

If there is an element c which already satisfies all the formulas in $\Sigma (x)$ , we say that c realizes $\Sigma (x)$ , and that $\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 $\phi (x;a)$ with a ∈ A, either

$\phi (x;a)\in p(x)$ or $\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 $\phi (x;a)$ with a ∈ A and $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

$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 S_n(A). This space is topologized by declaring the following set to be a basic open

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

for each formula $\phi (x;a)$ with a ∈ A.

With this topology, S_n(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 Mⁿ

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 Mⁿ to the two element boolean algebra {0,1}. This homomorphism sends a set of the form $\phi (M;a)$ to 1 if $\phi (x;a)\in p(x)$ and 0 otherwise.

Partial types over A essentially correspond to closed subsets of S_n(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 A ⊆ B ⊆ M, 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 $\phi (x;a)$ is in p|A' if and only if it is in p.

This yields a map on Stone spaces S_n(B) -> S_n(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

Any consistent partial type in M remains consistent as a partial type in N.
If A is a subset of M, then the complete n-types over A are the same when calculated in M as when calculated in N. Even the topological spaces are the same.
If a is a tuple from M and A is a subset of M, then tp(a/A) is the same when calculated in M as when calculated in N.
If a and b are two tuples from M, then the truth of $a\equiv _{A}b$ doesn't depend on whether the ambient model is M or N.

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

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

Proof: Let T be the union of $\Sigma (c)$ and the elementary diagram of M, where c is a new constant symbol not occurring in L(M). Any finite subset T₀ ⊆ T has a model, namely M with the constant symbol c realizing the finite part of $\Sigma (x)$ that appears in T₀. 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 $\Sigma (x)$ . QED.

This fact gives an alternative description of complete types:

$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 $\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 $\emptyset$ to complete quantifier-free n-types over $\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

${\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 $\Delta$ be a set of formulas of the form $\phi (x;y)$ with x a tuple of some fixed length. A ∆-formula over A is a boolean combination of formulas of the form $\phi (x;a)$ with a from A and $\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 $\{\phi (x;y)\}$ , one speaks of $\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.)

Examples[]

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

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

and

$\{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(x₁,...,x_n) over a set S ⊆ M, we must specify how each x_i compares to each element of S, and additionally, how x_i compares to x_j for i ≠ j.

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 K ⊆ M 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 $\mathbb {A} _{K}^{n}$ := Spec K[X₁,...X_n]), 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 x ∈ V and x ∉ W for W ∈ S. 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

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

such that no x in Mⁿ realized

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

This would imply that

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

But since each W_i 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

W contains V, in which case a and b are both on W (because both are in V)

W does not contain V, in which case W ∩ V is a proper closed K-subvariety of V, so by definition of p(x), neither a nor b is in W ∩ V. As both are in V, neither is in W.

Either way, we see that a ∈ W ⇔ b ∈ W. 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[X₁,...X_n] 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 W ∩ V is another. By minimality of V, we must have V ⊆ W. Therefore V is the unique smallest K-subvariety containing a.

If V were not K-irreducible, we could write V as a union V₁ ∪ V₂ of two strictly smaller closed subvarieties. Then one of V₁ or V₂ would contain a, contradicting minimality of V. QED_claim.

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.

QED.

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

The entire line.
0-dimensional irreducible varieties. These are finite sets of points, algebraic over K. K-irreducibility means that the set of points must be set of roots of some irreducible polynomial over K.

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 X² - 2 is the type of $\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 $V\times W$ is (usually) an irreducible variety over K as well. Can we describe the generic type of $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[X₁,...X_n]. Since this ring is Noetherian, each prime ideal is finitely generated. By basic cardinal arithmetic, there end up being only about $|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 $\kappa$ -stable for all $\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 $\aleph _{0}$ -stable. Replacing Q with appropriately chosen bigger total orders, one can prove that DLO is not $\kappa$ -stable for any $\kappa$ , so DLO is unstable. ::: ::: :::