Definition:Fork

From ProofWiki
Jump to navigation Jump to search

Definition

Let $T$ be a complete $\LL$-theory.

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

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

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



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


An individual formula $\map \phi {\bar x, \bar b}$ is said to fork if and only if the singleton $\set {\map \phi {\bar x, \bar b} }$ forks.


Note

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.