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

Forking is also related to a notion of independence: one says that tuples and are independent over a set if does not fork over . 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 , and let be a monster model. If is a small set of parameters and is a formula with parameters from , one says that **divides over ** if there is a -indiscernible sequence of realizations of such that is inconsistent. Alternatively, without mentioning indiscernible sequences, one can define dividing as follows: a formula is said to **-divide over **, for a positive integer, if there is a sequence of realizations of such that is -inconsistent, that is, such that any -element subset of is inconsistent.

A formula is said to **fork over ** if it implies a finite disjunction of formulas (with parameters from ) each of which divides over . That is, there is some and such that Any formula which divides over forks over , though there are examples of the converse failing.

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

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

In the theory of algebraically closed fields, forking turns out to be related to algebraic independence. If is an extension of fields (seen as substructures of the monster) and is a finite tuple, then it turns out that if and only if .

Forking is defined to ensure that it has the following extension property: if , any partial type over which does not fork over can be extended to a complete type over which does not fork over . Dividing does not have this property. In fact, a partial type can be extended to a global complete type which does not *divide* over if and only if the original type does not *fork* over . A global type divides over if and only if it forks over .

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

- doesn't divide over
- For every -indiscernible sequence beginning with , there is some such that is -indiscernible.

Forking has the following "left transitivity" property: if doesn't fork over and doesn't fork over , then doesn't fork over . In terms of independence, this means that and together imply . This is the mirror image of the more familiar kind of "right transitivity" which holds in simple theories: if doesn't fork over and doesn't fork over , then doesn't fork over . (In symbols: and imply .)

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

In general, any formula or type which divides over also forks over . 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 and with a ternary predicate interpreted as saying that or or , then the formula does not divide over , but does fork over . In complete detail, the formula implies the disjunction of the two formulas and . All tuples with have the same type over , and the sequence of formulas is -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 is a *model*, then a formula forks over if and only if it divides over . That is, forking and dividing agree over models. This holds more generally in NTP 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, never forks over . This comes from the easily verifiable fact that no formula over can divide over .

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

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

- doesn't divide over
- is Lascar -invariant. That is, for every formula and every and , if and have the same Lascar strong type over , then . Equivalently, is fixed by the group of Lascar strong automorphisms over .
- is -invariant. Equivalently, if is a formula and and have the same compact strong type over , then .

For stable theories, Lascar strong type, compact strong type, and strong type all agree, so one recovers the characterization of non-forking over as having an -invariant global extension.

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