Let M be a first-order
structure, A ⊆ M a subset of its universe,
φ(x,y) a formula in the language of M
in the tuples of variables x and y, and b a tuple of
variables from M of the appropriate length. We say that φ(x,b)
divides over A if there are
- a natural number k,
- an elementary extension N of
M, and
- an infinite sequence b0, b1, …
of realizations of the type of b over A
so that for any set K ⊂ ω of size k,
&capi ∈ K φ(N,bi)
= ∅
We say that the formula φ(x,b) forks over A
if it implies a finite disjunction of dividing formulae.
If A ⊆ B ⊆ M and p ∈ S(B) is a
type over B, then we say that p forks over A
if there is a forking formula in p. If a is a tuple
of elements from M, then we say that a is
free from B over A and write a ↓A B
if the type of a over B does not fork over
A.