In stability theory and its generalizations, forking is a way of making precise the notion of "generic extensions" of types and of independence. A formula which forks over a set of parameters {\displaystyle C} is thought of as being "non-generic." If {\displaystyle p} is a complete type over some set {\displaystyle C}, the non-forking extensions of {\displaystyle p} are those extensions which contain no formula forking over {\displaystyle C}; these are thought of as the "generic" extensions of {\displaystyle p}.

Forking is also related to a notion of independence: one says that tuples {\displaystyle a} and {\displaystyle b} are independent over a set {\displaystyle C} if {\displaystyle \operatorname {tp} (a/bC)} does not fork over {\displaystyle C}. This turns out to be a useful notion in the setting of stable theories, and their generalizations. In stable and simple theories, one has in particular the machinery of the forking calculus.


Fix some complete theory {\displaystyle T}, and let {\displaystyle \mathbb {U} } be a monster model. If {\displaystyle C} is a small set of parameters and {\displaystyle \phi (x;b)} is a formula with parameters from {\displaystyle \mathbb {U} }, one says that {\displaystyle \phi (x;b)} divides over {\displaystyle C} if there is a {\displaystyle C}-indiscernible sequence {\displaystyle \langle b_{i}\rangle _{i<\omega }} of realizations of {\displaystyle \operatorname {tp} (b/C)} such that {\displaystyle \bigwedge _{i<\omega }\phi (x;b_{i})} is inconsistent. Alternatively, without mentioning indiscernible sequences, one can define dividing as follows: a formula {\displaystyle \phi (x;b)} is said to {\displaystyle k}-divide over {\displaystyle C}, for {\displaystyle k} a positive integer, if there is a sequence {\displaystyle \langle b_{i}\rangle _{i<\omega }} of realizations of {\displaystyle \operatorname {tp} (b/C)} such that {\displaystyle \bigwedge _{i<\omega }\phi (x;b_{i})} is {\displaystyle k}-inconsistent, that is, such that any {\displaystyle k}-element subset of {\displaystyle \{\phi (x;b_{i})\}} is inconsistent.

A formula {\displaystyle \phi (x;b)} is said to fork over {\displaystyle C} if it implies a finite disjunction of formulas (with parameters from {\displaystyle \mathbb {U} }) each of which divides over {\displaystyle C}. That is, there is some {\displaystyle c_{i}\in \mathbb {U} } and {\displaystyle \psi _{i}(x;y)} such that {\displaystyle T\vdash \forall x:\phi (x;b)\rightarrow \bigvee _{i=1}^{n}\psi _{i}(x;c_{i})} Any formula which divides over {\displaystyle C} forks over {\displaystyle C}, though there are examples of the converse failing.

A partial type {\displaystyle \Sigma (x)} is said to fork over {\displaystyle C} (resp. divide over {\displaystyle C}) if it implies some formula which forks (resp. divides) over {\displaystyle C}. If {\displaystyle p} is a complete type over {\displaystyle C}, a non-forking extension of {\displaystyle p} is an extension which does not fork over {\displaystyle C}.

If {\displaystyle a} is a tuple and {\displaystyle B} and {\displaystyle C} are small sets, one says that {\displaystyle a} is (forking) independent from {\displaystyle B} over {\displaystyle C}, written {\displaystyle a\downarrow _{C}B}, if {\displaystyle \operatorname {tp} (a/BC)} doesn't fork over {\displaystyle C}, i.e., {\displaystyle \operatorname {tp} (a/BC)} is a non-forking extension of {\displaystyle \operatorname {tp} (a/B)}. If {\displaystyle A}, {\displaystyle B}, and {\displaystyle C} are small sets, then {\displaystyle A\downarrow _{C}B} means that {\displaystyle a\downarrow _{C}B} for every finite tuple {\displaystyle a} from {\displaystyle A}. In general, this notion is not symmetric: {\displaystyle A\downarrow _{C}B} need not be equivalent to {\displaystyle B\downarrow _{C}A}. Simple theories are exactly the theories for which this symmetry always holds; they include stable theories.

The case of ACF[]

In the theory of algebraically closed fields, forking turns out to be related to algebraic independence. If {\displaystyle L/K} is an extension of fields (seen as substructures of the monster) and {\displaystyle a} is a finite tuple, then it turns out that {\displaystyle a\downarrow _{K}L} if and only if {\displaystyle tr.deg(a/K)=tr.deg(a/L)}.

General properties of forking[]

Forking is defined to ensure that it has the following extension property: if {\displaystyle C'\supset C}, any partial type over {\displaystyle C'} which does not fork over {\displaystyle C} can be extended to a complete type over {\displaystyle C'} which does not fork over {\displaystyle C}. Dividing does not have this property. In fact, a partial type {\displaystyle \Sigma (x)} can be extended to a global complete type which does not divide over {\displaystyle C} if and only if the original type {\displaystyle \Sigma (x)} does not fork over {\displaystyle C}. A global type divides over {\displaystyle C} if and only if it forks over {\displaystyle C}.

Dividing can be defined more directly, in terms of indiscernible sequences. Specifically, the following are equivalent:

Forking has the following "left transitivity" property: if {\displaystyle \operatorname {tp} (a/BC)} doesn't fork over {\displaystyle C} and {\displaystyle \operatorname {tp} (a'/BCa)} doesn't fork over {\displaystyle Ca}, then {\displaystyle \operatorname {tp} (aa'/BC)} doesn't fork over {\displaystyle C}. In terms of independence, this means that {\displaystyle a\downarrow _{C}B} and {\displaystyle a'\downarrow _{Ca}B} together imply {\displaystyle aa'\downarrow _{C}B}. This is the mirror image of the more familiar kind of "right transitivity" which holds in simple theories: if {\displaystyle \operatorname {tp} (a/BC)} doesn't fork over {\displaystyle C} and {\displaystyle \operatorname {tp} (a/BB'C)} doesn't fork over {\displaystyle BC}, then {\displaystyle \operatorname {tp} (a/BB'C)} doesn't fork over {\displaystyle C}. (In symbols: {\displaystyle a\downarrow _{C}B} and {\displaystyle a\downarrow _{CB}B'} imply {\displaystyle a\downarrow _{C}BB'}.)

TODO: monotonicity, base monotonicity, finite character, normality, "rigidity."

Forking vs dividing[]

In general, any formula or type which divides over {\displaystyle C} also forks over {\displaystyle C}. The converse need not hold. The standard example of this is the theory of a dense circular order. If one considers the structure with underlying set {\displaystyle [0,1)\subset \mathbb {Q} } and with a ternary predicate {\displaystyle C(x,y,z)} interpreted as saying that {\displaystyle x<y<z} or {\displaystyle y<z<x} or {\displaystyle z<x<y}, then the formula {\displaystyle x=x} does not divide over {\displaystyle \emptyset }, but does fork over {\displaystyle \emptyset }. In complete detail, the formula {\displaystyle x=x} implies the disjunction of the two formulas {\displaystyle C(x,0,1/4)} and {\displaystyle C(x,1/2,3/4)}. All tuples {\displaystyle (b,c)} with {\displaystyle b\neq c} have the same type over {\displaystyle \emptyset }, and the sequence of formulas {\displaystyle C(x,1/2,1/3),C(x,1/3,1/4),C(x,1/4,1/5),\ldots } is {\displaystyle 2}-inconsistent. So forking is not the same as dividing in this theory.

On the other hand, it is known that forking and dividing agree in simple theories (including stable theories), o-minimal theories, and C-minimal theories (such as ACVF). Furthermore, in an NIP setting, it is proven by Chernikov and Kaplan that if {\displaystyle C} is a model, then a formula forks over {\displaystyle C} if and only if it divides over {\displaystyle C}. That is, forking and dividing agree over models. This holds more generally in NTP{\displaystyle {}_{2}} theories (again by Chernikov and Kaplan).

One useful consequence of forking=dividing (when it holds) is that no type forks over its base. That is, {\displaystyle \operatorname {tp} (a/C)} never forks over {\displaystyle C}. This comes from the easily verifiable fact that no formula over {\displaystyle C} can divide over {\displaystyle C}.

Forking in simple theories[]

In simple theories, one has the full machinery of the forking calculus. Forking satisfies symmetry: {\displaystyle A\downarrow _{C}B} is equivalent to {\displaystyle B\downarrow _{C}A}. This allows one to make definitions like Lascar rank, weight, independence, domination, and so on. Forking also satisfies local character: there is a cardinal {\displaystyle \kappa } such that for every finite tuple {\displaystyle a} and set {\displaystyle C}, there is some subset {\displaystyle C_{0}\subset C} such that {\displaystyle |C_{0}|<\kappa } and {\displaystyle a\downarrow _{C_{0}}C}. In other words, every type doesn't fork over some subtype of size bounded by {\displaystyle \kappa }.

Forking in NIP theories[]

In NIP theories, non-forking has an equivalent description in terms of Lascar or compact (KP) strong types. As in any theory, {\displaystyle \operatorname {tp} (a/BC)} doesn't fork over {\displaystyle C} if and only if {\displaystyle \operatorname {tp} (a/BC)} has an extension to a global type {\displaystyle p} which doesn't divide over {\displaystyle C}. In the NIP setting, however, it turns out that the following are equivalent for a global type {\displaystyle p}:

For stable theories, Lascar strong type, compact strong type, and strong type all agree, so one recovers the characterization of non-forking over {\displaystyle C} as having an {\displaystyle \operatorname {acl} ^{eq}(C)}-invariant global extension.

Forking in stable theories[]

Main article: Forking in stable theories. ::: ::: :::