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 $C$ is thought of as being "non-generic." If $p$ is a complete type over some set $C$ , the non-forking extensions of $p$ are those extensions which contain no formula forking over $C$ ; these are thought of as the "generic" extensions of $p$ .

Forking is also related to a notion of independence: one says that tuples $a$ and $b$ are independent over a set $C$ if $\operatorname {tp} (a/bC)$ does not fork over $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.

Definitions[]

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

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

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

If $a$ is a tuple and $B$ and $C$ are small sets, one says that $a$ is (forking) independent from $B$ over $C$ , written $a\downarrow _{C}B$ , if $\operatorname {tp} (a/BC)$ doesn't fork over $C$ , i.e., $\operatorname {tp} (a/BC)$ is a non-forking extension of $\operatorname {tp} (a/B)$ . If $A$ , $B$ , and $C$ are small sets, then $A\downarrow _{C}B$ means that $a\downarrow _{C}B$ for every finite tuple $a$ from $A$ . In general, this notion is not symmetric: $A\downarrow _{C}B$ need not be equivalent to $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 $L/K$ is an extension of fields (seen as substructures of the monster) and $a$ is a finite tuple, then it turns out that $a\downarrow _{K}L$ if and only if $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 $C'\supset C$ , any partial type over $C'$ which does not fork over $C$ can be extended to a complete type over $C'$ which does not fork over $C$ . Dividing does not have this property. In fact, a partial type $\Sigma (x)$ can be extended to a global complete type which does not divide over $C$ if and only if the original type $\Sigma (x)$ does not fork over $C$ . A global type divides over $C$ if and only if it forks over $C$ .

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

$\operatorname {tp} (A/bC)$ doesn't divide over $C$
For every $C$ -indiscernible sequence $I$ beginning with $b$ , there is some $I'\equiv _{bC}I$ such that $I'$ is $AC$ -indiscernible.

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

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

Forking vs dividing[]

In general, any formula or type which divides over $C$ also forks over $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 $[0,1)\subset \mathbb {Q}$ and with a ternary predicate $C(x,y,z)$ interpreted as saying that $x<y<z$ or $y<z<x$ or $z<x<y$ , then the formula $x=x$ does not divide over $\emptyset$ , but does fork over $\emptyset$ . In complete detail, the formula $x=x$ implies the disjunction of the two formulas $C(x,0,1/4)$ and $C(x,1/2,3/4)$ . All tuples $(b,c)$ with $b\neq c$ have the same type over $\emptyset$ , and the sequence of formulas $C(x,1/2,1/3),C(x,1/3,1/4),C(x,1/4,1/5),\ldots$ is $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 $C$ is a model, then a formula forks over $C$ if and only if it divides over $C$ . That is, forking and dividing agree over models. This holds more generally in NTP ${}_{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, $\operatorname {tp} (a/C)$ never forks over $C$ . This comes from the easily verifiable fact that no formula over $C$ can divide over $C$ .

Forking in simple theories[]

In simple theories, one has the full machinery of the forking calculus. Forking satisfies symmetry: $A\downarrow _{C}B$ is equivalent to $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 $\kappa$ such that for every finite tuple $a$ and set $C$ , there is some subset $C_{0}\subset C$ such that $|C_{0}|<\kappa$ and $a\downarrow _{C_{0}}C$ . In other words, every type doesn't fork over some subtype of size bounded by $\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, $\operatorname {tp} (a/BC)$ doesn't fork over $C$ if and only if $\operatorname {tp} (a/BC)$ has an extension to a global type $p$ which doesn't divide over $C$ . In the NIP setting, however, it turns out that the following are equivalent for a global type $p$ :

$p$ doesn't divide over $C$
$p$ is Lascar $C$ -invariant. That is, for every formula $\phi (x;y)$ and every $b$ and $b'$ , if $b$ and $b'$ have the same Lascar strong type over $C$ , then $\phi (x;b)\in p(x)\iff \phi (x;b')\in p(x)$ . Equivalently, $p(x)$ is fixed by the group of Lascar strong automorphisms over $C$ .
$p$ is $bdd(C)$ -invariant. Equivalently, if $\phi (x;y)$ is a formula and $b$ and $b'$ have the same compact strong type over $C$ , then $\phi (x;b)\in p(x)\iff \phi (x;b')\in p(x)$ .

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

Forking in stable theories[]

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