In stable structures, there is a canonical ternary relation on subsets of the structure, interpreted as " is independent from over ." There is also a closely connected notion of a "non-forking extension" of a complete type. This is related to as follows: if and is a tuple, is a non-forking extension of if , and is a forking extension of if . This depends only on and . 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 . 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 . The relation 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.

Work in a monster model of a stable theory . Recall that the **strong type** of over , denoted , is the type of over , the algebraic closure of in . In stable theories, strong types have canonical extensions: there is a unique complete type over which extends and which is -invariant. Denoting this unique extension by , one can make the following definition: if , then is a **non-forking extension** of if and only if It turns out that this definition depends only on and .

Then for , one defines to mean that for every finite , is a non-forking extension of .

See below for some alternative definitions.

- (symmetry)
- is equivalent to . That is, if is independent from over , then is independent from over .
- (invariance)
- If is an automorphism of , then . By strong homogeneity of the monster, this can be restated as follows: if , then . This is an unsurprising property, which would be expected of any definition which was canonical.
- (monotonicity)
- If and , then .
- (finite character)
- holds if and only if holds for all finite subsets and .
- (transitivity)
- If , then holds if and only if and hold. On the level of types, this means that is a non-forking extension of if and only if is a non-forking extension of and is a non-forking extension of . In particular, the relation of being a non-forking extension is transitive.
- (normality)
- is equivalent to . This means that really depends only on the set , and not on specifically.
- (stationarity)
- Suppose is a model, , , and . Then . On the level of types, this means that if and is a model, then every type over has a unique non-forking extension to .
- (existence)
- . On the level of types, this means that types are non-forking extensions of themselves.
- (full existence)
- Given we can find such that . On the level of types, this means that if , then every type over has at least one non-forking extension to .
- (local character)
- There is a cardinal such that if is finite and is arbitrary, then there exists with such that . 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 .

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 is a theory with monster model for which there exists a ternary relation satisfying the above axioms, then is stable and is forking independence.

Forking is closely related to ranks such as Morley rank and Lascar rank. If is one of Morley rank, Lascar rank, or Shelah infinity-rank, then governs forking, in the following sense: if is a type extending and , then

- if and only if is a non-forking extension of .
- if and only if is a forking extension of .

Equivalently, means that , and means that .

If has finite Lascar rank, can be defined very symmetrically as follows: means that for every finite tuple from and from ,

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 and , then .
- Because of symmetry, there are mirror-image versions of all the above properties. For example,
**left transitivity**says that if and , then . - If is a type over a model , the non-forking extensions of are exactly the same as the heirs of , which are in turn the same as the coheirs of .
- If is a type over a set which is algebraically closed in , then types over have unique non-forking extensions to larger sets. That is, if and and , then . Thus, strong types are stationary.
- Whether or not holds depends only on , , and :
- Forking is always witnessed by a formula: if is a forking extension of (i.e., ), then there is a -formula such that every type extending is a forking extension of its restriction to . One says that
**forks over**when this property holds. So, we are saying that if and only if no formula in forks over . - If and is some other set, we can find such that . On the level of types, this means that if and is a type on which has some non-forking extension to , then can be further extended to a type on which is a non-forking extension of . This fact is called
**extension**, and is an easy consequence of transitivity and full existence. - If , and , then . This is a consequence of transitivity, as we have stated it above. This fact is usually called
**base monotonicity**. - One says that a sequence of sets is
**independent**over if for each , So is independent over if , , , and so on. The fundamental fact about this notion is that whether or not a sequence is independent over*does not depend on the order of the terms*, that is, any permutation of an independent sequence is still independent. For example, if and , we can conclude that . - Any subsequence of a -independent sequence is still -independent, and an infinite sequence is -independent if and only if every finite subsequence is -independent.
- If is an independent sequence of tuples over , and , , and are three pairwise disjoint subsequences, then . For example, if is independent over , then .
- If is -independent, and is some finite tuple, then must hold for all but at most values of , where is the cardinal from the local character property.
- Independence is preserved in non-forking extensions: if and is a non-forking extension of (that is, , then More generally, if is a sequence, , and , then is -independent if and only if it is -independent.

There are a number of different approaches to defining non-forking and , 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 and are finite, means that where denotes the product operation on global invariant types. Alternatively, means that for two -definable global types and . Either way, is then defined to mean that for every finite and . Then is a non-forking extension of if and only if .

Shelah's original definition of forking proceeds as follows. A formula is said to **divide** over a set if there exists a -indiscernible sequence of realizations of such that is inconsistent. A formula is said to **fork** over a set if it implies a finite disjunction of formulas (with parameters from ), such that each divides over . A type forks (divides) over if some formula in it forks (divides) over .

Then one defines to mean that doesn’t fork over for every finite tuple from . In a stable theory, it turns out that one can equivalently replace "forking" with "dividing" in this definition. Shelah’s definition of is somewhat convoluted, but turns out to be the right definition for use with unstable theories, such as simple theories, NIP theories, and NTP_{2} theories.

In Poizat’s *Course in Model Theory* a different definition of forking is given for stable theories, using the fundamental order. If is a complete type over a model, we say that a formula is "represented" in if for some . If and are two complete types over models, we say that if every formula represented in is also represented in . If is an extension of , then holds, for example. This defines a pre-order on the class of types over models; the quotient poset is called the **fundamental order**. If is a type over an arbitrary set , and is a model, then among the equivalence classes of extensions of to , there is a unique maximum in the fundamental order. This maximum is called the **bound** of ; it does not depend on . Now if and are two complete types, and is an extension of , then is a non-forking extension of if and only if and have the same bound. So means that for every finite tuple from , and have the same bound.

In totally transcendental theories, as noted above, is a non-forking extension of if and only if . 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 .

In a general stable theory, there is still a way to define using ranks. If is a finite set of formulas, and is a finite partial type, the local -rank is defined to be the Cantor-Bendixson rank of the space of -types over which are consistent with . If is an arbitrary partial type, is defined to be the minimum of , for a finite subtype of . In a stable theory, always holds. If is a type extending (complete types over different sets), then it turns out that is a non-forking extension of if and only if for every finite set of formulas . ::: ::: :::