From ProofWiki
Jump to navigation Jump to search


Let $T$ be a complete $\mathcal{L}$-theory.

Let $\mathfrak{C}$ be a monster model for $T$.

Let $A$ be a subset of the universe of $\mathfrak{C}$.

Let $\pi (\bar{x}, \bar{b})$ be a set of $\mathcal{L}$-formulas with free variables $\bar{x}$ and parameters $\bar{b}$ from the universe of $\mathfrak{C}$.

$\pi(\bar{x}, \bar{b})$ forks over $A$ if it implies some disjunction $\phi_1 (\bar x, \bar c_1) \vee \cdots \vee \phi_n (\bar x, \bar c_n)$ where each $\phi_i (\bar x, \bar c_i)$ divides over $A$.

An individual formula $\phi (\bar x, \bar b)$ is said to fork if the singleton $\{\phi (\bar x, \bar b)\}$ forks.


The advantage in discussing forking rather than dividing is in theorems like Formula and its Negation Cannot Both Cause Forking, which play a part in allowing us to extend non-forking types to complete non-forking types.