Forking is Local

This article needs to be linked to other articles. You can help $\mathsf{Pr} \infty \mathsf{fWiki}$ by adding these links. To discuss this page in more detail, feel free to use the talk page. When this work has been completed, you may remove this instance of {{MissingLinks}} from the code.

Theorem

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

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

Let $A\subseteq B$ be subsets of the universe of $\mathfrak C$.

Let $\map \pi {\bar x}$ be an $n$-type over $B$.

$\pi$ forks over $A$ if and only if a finite subset of $\pi$ forks over $A$.

Proof

Suppose $\pi$ forks over $A$.

By definition, $\pi$ implies a disjunction of formulas which each divide over $A$.

Since proofs are finite, this means that there is a finite subset of $\pi$ which implies this disjunction, completing this direction of the proof.

Suppose a finite subset of $\pi$ forks over $A$.

By definition, the finite subset implies a disjunction of formulas which each divide over $A$.

But then $\pi$ clearly implies this disjunction as well, completing this direction of the proof.

$\blacksquare$