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.
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
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:
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 NTP2 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
. ::: ::: :::