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 Edit

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) $ 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 Edit

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 Edit

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 Edit

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 \ne 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 Edit

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 Edit

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 Edit

Main article: Forking in stable theories.