In stable structures, there is a canonical ternary relation $A\downarrow _{C}B$ on subsets $A,B,C$ of the structure, interpreted as " $A$ is independent from $B$ over $C$ ." There is also a closely connected notion of a "non-forking extension" of a complete type. This is related to $\downarrow$ as follows: if $C\subset B$ and $a$ is a tuple, $\operatorname {tp} (a/B)$ is a non-forking extension of $\operatorname {tp} (a/C)$ if $a\downarrow _{C}B$ , and is a forking extension of $\operatorname {tp} (a/C)$ if $a\not \downarrow _{C}B$ . This depends only on $\operatorname {tp} (a/B)$ and $\operatorname {tp} (a/C)$ . The non-forking extensions of a complete type can be thought of as the "generic" or "canonical" extensions, in a certain sense.

The ternary independence relation and the relation of non-forking can be defined through several different approaches, described below. In practice, what is more important than the definition is the formal properties possessed by these relations. In fact, these properties can be used to axiomatize $\downarrow$ . The manipulation of independence and non-forking via these axioms and other properties is called the forking calculus. Forking computations play a key role in many proofs in stability theory.

In superstable theories, forking is closely connected to ranks such as Lascar rank and Morley rank. In a general stable theory, these ranks may explode. Certain arguments that work in superstable settings can be generalized to stable theories through reformulation in terms of $\downarrow$ . The relation $\downarrow$ also appears in many of the basic definitions of stability theory, such as Lascar rank, stationary types, orthogonal types, regular types, domination, and weight.

Forking calculus in stable theories can be generalized to simple theories, and more generally, rosy theories. Along the way, one or two of the axioms must be dropped, however.

Definitions[]

Work in a monster model $\mathbb {U}$ of a stable theory $T$ . Recall that the strong type of $a$ over $C$ , denoted $\operatorname {stp} (a/C)$ , is the type of $a$ over $\operatorname {acl} ^{eq}(C)$ , the algebraic closure of $C$ in $\mathbb {U} ^{eq}$ . In stable theories, strong types have canonical extensions: there is a unique complete type $p$ over $\mathbb {U}$ which extends $\operatorname {stp} (a/C)$ and which is $\operatorname {Aut} (\mathbb {U} /\operatorname {acl} ^{eq}(C))$ -invariant. Denoting this unique extension by $\operatorname {stp} (a/C)|\mathbb {U}$ , one can make the following definition: if $C\subset B$ , then $\operatorname {tp} (a/B)$ is a non-forking extension of $\operatorname {tp} (a/C)$ if and only if $\operatorname {stp} (a/B)|\mathbb {U} =\operatorname {stp} (a/C)|\mathbb {U} .$ It turns out that this definition depends only on $\operatorname {tp} (a/C)$ and $\operatorname {tp} (a/B)$ .

Then for $A,B,C\subset \mathbb {U}$ , one defines $A\downarrow _{C}B$ to mean that for every finite $a\subset A$ , $\operatorname {tp} (a/BC)$ is a non-forking extension of $\operatorname {tp} (a/C)$ .

See below for some alternative definitions.

Axioms and Basic Properties[]

(symmetry): $A\downarrow _{C}B$ is equivalent to $B\downarrow _{C}A$ . That is, if $A$ is independent from $B$ over $C$ , then $B$ is independent from $A$ over $C$ .
(invariance): If $\sigma$ is an automorphism of $\mathbb {U}$ , then $A\downarrow _{C}B\iff \sigma (A)\downarrow _{\sigma (C)}\sigma (B)$ . By strong homogeneity of the monster, this can be restated as follows: if $A'B'C'\equiv _{\emptyset }ABC$ , then $A'\downarrow _{C'}B'\iff A\downarrow _{C}B$ . This is an unsurprising property, which would be expected of any definition which was canonical.
(monotonicity): If $A'\subset A$ and $B'\subset B$ , then $A\downarrow _{C}B\implies A'\downarrow _{C}B'$ .
(finite character): $A\downarrow _{C}B$ holds if and only if $A'\downarrow _{C}B'$ holds for all finite subsets $A'\subset A$ and $B'\subset B$ .
(transitivity): If $B_{1}\subset B_{2}\subset B_{3}$ , then $A\downarrow _{B_{1}}B_{3}$ holds if and only if $A\downarrow _{B_{1}}B_{2}$ and $A\downarrow _{B_{2}}B_{3}$ hold. On the level of types, this means that $\operatorname {tp} (A/B_{3})$ is a non-forking extension of $\operatorname {tp} (A/B_{1})$ if and only if $\operatorname {tp} (A/B_{3})$ is a non-forking extension of $\operatorname {tp} (A/B_{2})$ and $\operatorname {tp} (A/B_{2})$ is a non-forking extension of $\operatorname {tp} (A/B_{1})$ . In particular, the relation of being a non-forking extension is transitive.
(normality): $A\downarrow _{C}B$ is equivalent to $A\downarrow _{C}BC$ . This means that $A\downarrow _{C}B$ really depends only on the set $BC$ , and not on $B$ specifically.
(stationarity): Suppose $M$ is a model, $A\downarrow _{M}B$ , $A'\downarrow _{M}B$ , and $A\equiv _{M}A'$ . Then $A\equiv _{MB}A'$ . On the level of types, this means that if $M\subset B$ and $M$ is a model, then every type over $M$ has a unique non-forking extension to $B$ .
(existence): $A\downarrow _{B}B$ . On the level of types, this means that types are non-forking extensions of themselves.
(full existence): Given $A,B,C$ we can find $A'\equiv _{C}A$ such that $A'\downarrow _{C}B$ . On the level of types, this means that if $C\subset B$ , then every type over $C$ has at least one non-forking extension to $B$ .
(local character): There is a cardinal $\kappa$ such that if $A$ is finite and $C$ is arbitrary, then there exists $C'\subset C$ with $|C'|<\kappa$ such that $A\downarrow _{C'}C$ . On the level of types, this means that every type is a non-forking extension of some type over a set of size less than $\kappa$ .

Some of the above properties, such as symmetry, are more readily expressed in terms of independence, while others, such as transitivity, are more readily expressed in terms of non-forking extensions. Part of the complexity of forking calculus comes from the interplay of these two notions.

The above conditions actually characterize stable theories, in the following sense: if $T$ is a theory with monster model $\mathbb {U}$ for which there exists a ternary relation $\downarrow$ satisfying the above axioms, then $T$ is stable and $\downarrow$ is forking independence.

Forking and ranks[]

Forking is closely related to ranks such as Morley rank and Lascar rank. If $R(-)$ is one of Morley rank, Lascar rank, or Shelah infinity-rank, then $R(-)$ governs forking, in the following sense: if $p(x)$ is a type extending $q(x)$ and $R(q)<\infty$ , then

$R(p)=R(q)$ if and only if $p(x)$ is a non-forking extension of $q(x)$ .
$R(p)<R(q)$ if and only if $p(x)$ is a forking extension of $q(x)$ .

Equivalently, $a\downarrow _{C}B$ means that $R(a/BC)=R(a/C)$ , and $a\not \downarrow _{C}B$ means that $R(a/BC)<R(a/C)$ .

If $T$ has finite Lascar rank, $\downarrow$ can be defined very symmetrically as follows: $A\downarrow _{C}B$ means that for every finite tuple $a$ from $A$ and $b$ from $B$ , $U(ab/C)=U(a/C)+U(b/C).$

Further properties[]

Aside from the axioms listed above, there are a number of other commonly used properties of forking:

By throwing in normality, transitivity can be slightly strengthened to the following statement: if $A\downarrow _{C}B$ and $A\downarrow _{CB}B'$ , then $A\downarrow _{C}BB'$ .
Because of symmetry, there are mirror-image versions of all the above properties. For example, left transitivity says that if $A\downarrow _{C}B$ and $A'\downarrow _{CA}B$ , then $AA'\downarrow _{C}B$ .
If $p$ is a type over a model $M$ , the non-forking extensions of $p$ are exactly the same as the heirs of $p$ , which are in turn the same as the coheirs of $p$ .
If $p$ is a type over a set $C=\operatorname {acl} ^{eq}(C)$ which is algebraically closed in $\mathbb {U} ^{eq}$ , then types over $C$ have unique non-forking extensions to larger sets. That is, if $A\downarrow _{C}B$ and $A'\downarrow _{C}B$ and $A\equiv _{C}A'$ , then $A\equiv _{BC}A'$ . Thus, strong types are stationary.
Whether or not $A\downarrow _{C}B$ holds depends only on $\operatorname {acl} (A)$ , $\operatorname {acl} (C)$ , and $\operatorname {acl} (B)$ : $A\downarrow _{C}B\iff \operatorname {acl} (A)\downarrow _{\operatorname {acl} (C)}\operatorname {acl} (B)\iff \operatorname {acl} (AC)\downarrow _{\operatorname {acl} (C)}\operatorname {acl} (BC)$
Forking is always witnessed by a formula: if $\operatorname {tp} (a/BC)$ is a forking extension of $\operatorname {tp} (a/C)$ (i.e., $a\not \downarrow _{C}B$ ), then there is a $BC$ -formula $\phi (x)\in \operatorname {tp} (a/BC)$ such that every type extending $\phi (x)$ is a forking extension of its restriction to $C$ . One says that $\phi (x)$ forks over $C$ when this property holds. So, we are saying that $a\downarrow _{C}B$ if and only if no formula in $\operatorname {tp} (a/BC)$ forks over $C$ .
If $A\downarrow _{C}B$ and $D$ is some other set, we can find $A'\equiv _{BC}A$ such that $A'\downarrow _{C}BD$ . On the level of types, this means that if $C\subset B\subset D$ and $p$ is a type on $C$ which has some non-forking extension $q$ to $B$ , then $q$ can be further extended to a type on $D$ which is a non-forking extension of $p$ . This fact is called extension, and is an easy consequence of transitivity and full existence.
If $A\downarrow _{C}B$ , and $D\subset B$ , then $A\downarrow _{CD}B$ . This is a consequence of transitivity, as we have stated it above. This fact is usually called base monotonicity.
One says that a sequence $\{A_{\alpha }\}_{\alpha <\lambda }$ of sets is independent over $C$ if for each $\alpha$ , $A_{\alpha }\downarrow _{C}A_{<\alpha },{\text{ where }}A_{<\alpha }=\bigcup _{\beta <\alpha }A_{\beta }.$ So $a_{1},a_{2},\ldots$ is independent over $C$ if $a_{1}\downarrow _{C}a_{2}$ , $a_{1}a_{2}\downarrow _{C}a_{3}$ , $a_{1}a_{2}a_{3}\downarrow _{C}a_{4}$ , and so on. The fundamental fact about this notion is that whether or not a sequence is independent over $C$ does not depend on the order of the terms, that is, any permutation of an independent sequence is still independent. For example, if $a_{1}\downarrow _{C}a_{2}$ and $a_{1}a_{2}\downarrow _{C}a_{3}$ , we can conclude that $a_{2}a_{3}\downarrow _{C}a_{1}$ .
Any subsequence of a $C$ -independent sequence is still $C$ -independent, and an infinite sequence is $C$ -independent if and only if every finite subsequence is $C$ -independent.
If $I$ is an independent sequence of tuples over $C$ , and $I_{1}$ , $I_{2}$ , and $I_{3}$ are three pairwise disjoint subsequences, then $I_{1}\downarrow _{CI_{2}}I_{3}$ . For example, if $a_{1},a_{2},a_{3}$ is independent over $\emptyset$ , then $a_{1}\downarrow _{a_{2}}a_{3}$ .
If $\{A_{\alpha }\}_{\alpha <\lambda }$ is $C$ -independent, and $b$ is some finite tuple, then $b\downarrow _{C}A_{\alpha }$ must hold for all but at most $\kappa$ values of $\alpha$ , where $\kappa$ is the cardinal from the local character property.
Independence is preserved in non-forking extensions: if $C\subset C'$ and $\operatorname {tp} (AB/C')$ is a non-forking extension of $\operatorname {tp} (AB/C)$ (that is, $AB\downarrow _{C}C'$ , then $A\downarrow _{C}B\iff A\downarrow _{C'}B.$ More generally, if $A_{1},A_{2},\ldots$ is a sequence, $C\subset C'$ , and $A_{1}A_{2}\cdots \downarrow _{C}C'$ , then $A_{1},A_{2},\ldots$ is $C$ -independent if and only if it is $C'$ -independent.

Alternative Definitions[]

There are a number of different approaches to defining non-forking and $\downarrow$ , aside from the one used above. All these definitions agree, for stable theories.

As a slight variant of the definition given above, one can proceed as follows. If $a$ and $b$ are finite, $a\downarrow _{C}b$ means that $(\operatorname {stp} (a/C)|\mathbb {U} )\otimes (\operatorname {stp} (b/C)|\mathbb {U} )=\operatorname {stp} (ab/C)|\mathbb {U} ,$ where $\otimes$ denotes the product operation on global invariant types. Alternatively, $a\downarrow _{C}b$ means that $ab\models (p\otimes q)|C$ for two $\operatorname {acl} ^{eq}(C)$ -definable global types $p$ and $q$ . Either way, $A\downarrow _{C}B$ is then defined to mean that $a\downarrow _{C}b$ for every finite $a\subset A$ and $b\subset B$ . Then $\operatorname {tp} (a/BC)$ is a non-forking extension of $\operatorname {tp} (a/C)$ if and only if $a\downarrow _{C}B$ .

Shelah's original definition of forking proceeds as follows. A formula $\phi (x;a)$ is said to divide over a set $C$ if there exists a $C$ -indiscernible sequence $a_{1},a_{2},\ldots$ of realizations of $\operatorname {tp} (a/C)$ such that $\bigwedge _{i=1}^{\infty }\phi (x;a_{i})$ is inconsistent. A formula $\phi (x;a)$ is said to fork over a set $C$ if it implies a finite disjunction $\bigvee _{j=1}^{n}\psi _{j}(x;b_{j})$ of formulas (with parameters $b_{j}$ from $\mathbb {U}$ ), such that each $\psi _{j}(x;b_{j})$ divides over $C$ . A type $\Sigma (x)$ forks (divides) over $C$ if some formula in it forks (divides) over $C$ .

Then one defines $A\downarrow _{C}B$ to mean that $\operatorname {tp} (a/BC)$ doesn’t fork over $C$ for every finite tuple $a$ from $A$ . In a stable theory, it turns out that one can equivalently replace "forking" with "dividing" in this definition. Shelah’s definition of $\downarrow$ is somewhat convoluted, but turns out to be the right definition for use with unstable theories, such as simple theories, NIP theories, and NTP₂ theories.

In Poizat’s Course in Model Theory a different definition of forking is given for stable theories, using the fundamental order. If $p(x)$ is a complete type over a model, we say that a formula $\phi (x;y)$ is "represented" in $p(x)$ if $\phi (x;a)\in p(x)$ for some $a$ . If $p(x)$ and $q(x)$ are two complete types over models, we say that $p\leq q$ if every formula represented in $q$ is also represented in $p$ . If $p$ is an extension of $q$ , then $p\leq q$ holds, for example. This defines a pre-order on the class of types over models; the quotient poset is called the fundamental order. If $p$ is a type over an arbitrary set $A$ , and $M\supset A$ is a model, then among the equivalence classes of extensions of $p$ to $M$ , there is a unique maximum in the fundamental order. This maximum is called the bound of $p$ ; it does not depend on $M$ . Now if $p$ and $q$ are two complete types, and $q$ is an extension of $p$ , then $q$ is a non-forking extension of $p$ if and only if $q$ and $p$ have the same bound. So $A\downarrow _{C}B$ means that for every finite tuple $a$ from $A$ , $\operatorname {tp} (a/BC)$ and $\operatorname {tp} (a/C)$ have the same bound.

In totally transcendental theories, as noted above, $\operatorname {tp} (a/BC)$ is a non-forking extension of $\operatorname {tp} (a/C)$ if and only if $RM(a/BC)=RM(a/C)$ . This can be used to define non-forking, in a totally transcendental setting. The analogous fact for Lascar rank in superstable theories cannot really be used as a definition, because Lascar rank is (usually) defined in terms of $\downarrow$ .

In a general stable theory, there is still a way to define $\downarrow$ using ranks. If $\Delta$ is a finite set of formulas, and $\Sigma (x)$ is a finite partial type, the local $\Delta$ -rank $R(\Sigma (x);\Delta ;\omega )$ is defined to be the Cantor-Bendixson rank of the space of $\Delta$ -types over $\mathbb {U}$ which are consistent with $\Sigma (x)$ . If $\Sigma (x)$ is an arbitrary partial type, $R(\Sigma (x);\Delta ;\omega )$ is defined to be the minimum of $R(\Sigma _{0}(x);\Delta ;\omega )$ , for $\Sigma _{0}(x)$ a finite subtype of $\Sigma (x)$ . In a stable theory, $R(\Sigma (x);\Delta ;\omega )<\infty$ always holds. If $p(x)$ is a type extending $q(x)$ (complete types over different sets), then it turns out that $p$ is a non-forking extension of $q$ if and only if $R(p;\Delta ;\omega )=R(q;\Delta ;\omega )$ for every finite set of formulas $\Delta$ . ::: ::: :::