Work in a stable theory $T$ with monster model $\mathbb {U}$ .

This article continues where Proofs:Equivalent Definitions of Stability leaves off. We will make use of the following fact from that page:

Fact. Let $p(x)$ be a type over a set $A$ . Let $\phi (x;y)$ be a formula. Then there is at least one $q(x)\in S_{\phi }(\mathbb {U} )$ which is consistent with $p(x)$ and which has finite orbit under $\operatorname {Aut} (\mathbb {U} /A)$ .

Strong Types Have Canonical Extensions[]

If $T$ is stable, so is $T^{eq}$ . To see this, let $\phi (x;y)$ be a formula in $T^{eq}$ . Then $x$ and $y$ come from sorts of the form $X_{1}/E_{1}$ and $X_{2}/E_{2}$ , where $X_{1}$ and $X_{2}$ are sorts (or products of sorts) in $T$ , and $E_{1}$ and $E_{2}$ are definable equivalence relations on $X_{1}$ and $X_{2}$ . Let $\pi _{i}:X_{i}\to X_{i}/E_{i}$ be the natural projection map, and let $\psi (z;w)=\phi (\pi _{1}(z);\pi _{2}(w))$ . Then $\psi (z;w)$ is (equivalent to) a formula in $T$ , so it does not have the order property. If $\phi (x;y)$ has the order property, then there exist $a_{i},b_{i}$ for $i<\omega$ such that $\models \phi (a_{i};b_{j})$ if and only if $i<j$ . Choosing $c_{i}\in \pi _{1}^{-1}(a_{i})$ and $d_{i}\in \pi _{2}^{-1}(b_{i})$ , we get that $\models \psi (c_{i};d_{j})$ if and only if $i<j$ , a contradiction.

Assume for the rest of this section that $T$ is a stable theory with elimination of imaginaries. (If $T$ is stable without elimination of imaginaries, replace $T$ with $T^{eq}$ .) The assumption that we have elimination of imaginaries will be used mainly in the following way:

Observation 1. Let $A$ be a small algebraically closed set, $\operatorname {acl} (A)=A$ . Let $X$ be a definable set. Suppose $X$ has finitely many conjugates under $\operatorname {Aut} (\mathbb {U} /A)$ . Then $X$ is $A$ -definable, and hence has a unique conjugate under $\operatorname {Aut} (\mathbb {U} /A)$ .

Proof. If $[X]$ is a code for $X$ , then $[X]$ has finitely many conjugates over $A$ , hence is in $\operatorname {acl} (A)=A$ . Since $X$ is $[X]$ -definable, $X$ is $A$ -definable. QED

Lemma. Let $A=\operatorname {acl} (A)$ be a small set. Let $p(x)$ be a complete type over $A$ and let $\phi (x;y)$ be a formula. Then there is a global $\phi$ -type which is $A$ -invariant (i.e., $\operatorname {Aut} (\mathbb {U} /A)$ -invariant), and which is consistent with $p(x)$ .

Proof. By the fact at the beginning of this page, we can find a global $\phi$ -type $q$ which is consistent with $p(x)$ and has finitely many conjugates over $A$ . Now if $\psi (y)$ is the $\phi$ -definition of $q(x)$ , that is, $\phi (x;b)\in q(x)\iff \models \psi (b)$ for every $q(x)$ , then the $\mathbb {U}$ -definable set $\psi (\mathbb {U} )$ has finitely many conjugates over $A$ . By Observation 1, $\psi (y)$ must be $A$ -definable. So $q(x)$ is $A$ -invariant. QED

Recall that if $\phi _{1}(x;y)$ and $\phi _{2}(x;z)$ are two formulas, we can find a third formula $\psi (x;w)$ such that the sets of the form $\psi (\mathbb {U} ;c)$ are precisely the sets of the form $\phi _{1}(\mathbb {U} ;a)$ and $\phi _{2}(\mathbb {U} ;b)$ . Specifically, we take $\psi (x;y,z,w',w'')$ to be $(\phi _{1}(x;y)\wedge (w'=w''))\vee (\phi _{2}(x;y)\wedge (w'\neq w''))$ So $\psi$ acts like $\phi _{1}$ if the dummy variables $w'$ and $w''$ agree, and acts like $\phi _{2}$ if they do not agree.

Iterating this, one sees that given $\phi _{1}(x;y_{1}),\ldots ,\phi _{n}(x;y_{n})$ , we can find $\psi (x;w)$ such that the formulas of the form $\psi (\mathbb {U} ;c)$ are exactly the formulas of the form $\phi _{i}(x;b)$ for some $i$ and $b$ . Consequently, given a finite set of formulas $\Delta$ , we can find a single formula $\psi$ such that $\Delta$ -formulas are the same thing as $\phi$ -formulas, and consequently $\Delta$ -types are the same thing as $\psi$ -types.

By the previous lemma, we conclude that if $\Delta$ is a finite set of formulas, if $A=\operatorname {acl} (A)$ , and if $p(x)$ is a complete type over $A$ , then there is a global $\Delta$ -type which is consistent with $p(x)$ and $A$ -invariant.

From this, it essentially follows by compactness that types over algebraically closed sets have global invariant extensions:

Lemma. Let $A=\operatorname {acl} (A)$ be a small set. Let $p(x)$ be a complete type over $A$ . Then there is a global $A$ -invariant complete type $p'(x)$ extending $p(x)$ . The type $p'(x)$ is $A$ -definable.

Proof. Let $\Sigma (x)$ be the partial type over $\mathbb {U}$ asserting that for every formula $\phi (x;y)$ , and every $b\equiv _{A}c$ , $\phi (x;b)\leftrightarrow \phi (x;c)$ Then $p(x)\cup \Sigma (x)$ is consistent. To see this, for each finite set of formulas $\Delta$ , let $\Sigma _{\Delta }(x)$ assert that $\phi (x;b)\leftrightarrow \phi (x;c)$ for every $\phi \in \Delta$ and every $b\equiv _{A}c$ . Then $\Sigma (x)$ is the union of the $\Sigma _{\Delta }(x)$ ’s as $\Delta$ ranges over bigger and bigger sets, so it suffices to see that $p(x)\cup \Sigma _{\Delta }(x)$ is consistent for each $\Delta$ . But this follows from the fact that there is a global $A$ -invariant $\Delta$ -type which is consistent with $p(x)$ .

So $p(x)\cup \Sigma (x)$ is consistent. If $p'(x)$ is any complete type extending it, then $p'(x)$ is $A$ -invariant.

By stability, $p(x)$ is definable. For each formula $\phi$ , the $\phi$ -definition of $p(x)$ is $A$ -invariant, hence $A$ -definable. So $p(x)$ is $A$ -definable. QED

In fact, the type $p'(x)$ is uniquely determined by $p(x)$ . To prove this, we will need a preliminary version of the symmetry of forking.

Recall that if $p(x)$ and $q(y)$ are two global $A$ -invariant types (in any theory), there is a well-defined global $A$ -invariant type $p(x)\otimes q(y)$ which is characterized by the fact that for any $B$ , the following are equivalent:

$(a,b)\models (p\otimes q)|B$ .
$b\models q|B$ and $a\models p|Bb$ .

Theorem 2. Let $A$ be a small set of parameters. Let $p(x)$ and $q(y)$ be two global $A$ -definable types. Then $p(x)\otimes q(y)=q(y)\otimes p(x)$ .

Proof. If not, there is some formula $\phi (x;y;c)$ which belongs to $p(x)\otimes q(y)$ but not to $q(y)\otimes p(x)$ . Let $a_{i},b_{i}$ be a sequence recursively constructed as follows:

$b_{i}$ is a realization of $q$ restricted to $Ac\cup \{a_{j}:j<i\}\cup \{b_{j}:j<i\}$
$a_{i}$ is a realization of $p$ restricted to $Ac\cup \{a_{j}:j<i\}\cup \{b_{j}:j\leq i\}$ .

So essentially the sequence $b_{1},a_{1},b_{2},a_{2},\ldots$ is a realization of $(q\otimes p\otimes q\otimes p\otimes \cdots )|Ac$ .

If $i<j$ , then $(a_{i};b_{j})\models (p\otimes q)|Ac$ , so $\phi (a_{i};b_{j};c)$ holds. On the other hand, if $i\geq j$ , then $(b_{j};a_{i})\models (q\otimes p)|Ac$ , so $\phi (a_{i};b_{j};c)$ does not hold. Therefore $\phi (x;y,z)$ has the order property, a contradiction. QED

Corollary 3. Let $A=\operatorname {acl} (A)$ . Then each complete type over $A$ has a unique global $A$ -invariant extension.

Proof. Let $p$ and $p'$ be two global $A$ -invariant types such that $p|A=p'|A$ . Suppose $p\neq p'$ . Then there is some formula $\phi (x;b)$ which is in $p$ but not in $p'$ . Let $a$ realize $p|Ab$ and $a'$ realize $p|Ab'$ . Then $\phi (a;b)$ holds and $\phi (a';b)$ does not, so $(a,b)\not \equiv _{A}(a',b)$ .

Let $q$ be a global $A$ -invariant type extending $\operatorname {tp} (b/A)$ . Note that $(a,b)\models (p\otimes q)|A$ and $(a',b)\models (p'\otimes q)|A$ . By Lemma 2, $(b,a)\models (q\otimes p)|A$ and $(b,a')\models (q\otimes p')|A$ . Now $(q\otimes p)|A$ depends on $p$ only through $p|A$ , so we should in fact have $(q\otimes p)|A=(q\otimes p')|A$ , contradicting $(a,b)\not \equiv _{A}(a',b)$ .

More precisely, let $\sigma$ be an automorphism over $A$ moving $a'$ to $a$ . Since $b\models q|Aa'$ , and $q$ is fixed by $\sigma$ , we get that $\sigma (b)\models q|Aa$ . As $b\models q|Aa$ , we get that $\sigma (b)\equiv _{Aa}b$ , or equivalently, $(a,b)\equiv _{A}(a,\sigma (b))=\sigma ((a',b))$ . So $(a,b)\equiv _{A}(a',b)$ , a contradiction. QED

Although we have proven Corollary 3 for finitary types, it holds equally well for infinitary types, by an easy exercise. One way to see this is to verify that the above proof works for infinitary types. (Infinitary $\phi$ -types turn out to be equivalent to finitary $\phi$ -types, because a single formula $\phi$ can only reference finitely many of the variables in an infinite tuple.) Alternatively, one can deduce Corollary 3 for infinitary types from Corollary 3 for finitary types, by using the fact that $S_{I}(A)=\lim _{\rightarrow }S_{I_{0}}(A)$ where the limit ranges over finite subsets $I_{0}$ of $I$ , and $S_{I}(A)$ denotes the set of complete types over $A$ of tuples $\langle a_{i}\rangle _{i\in I}$ indexed by $I$ .

Forking[]

Suppose $T$ is stable, but perhaps does not eliminate imaginaries. If $C$ is a small subset of the monster $\mathbb {U}$ , or of $\mathbb {U} ^{eq}$ , then $\operatorname {acl} ^{eq}(C)$ denotes the algebraic closure of $C$ within $\mathbb {U} ^{eq}$ .

If $a$ is a tuple, the strong type of $a$ over $C$ , denoted $\operatorname {stp} (a/C)$ is by definition just $\operatorname {tp} (a/\operatorname {acl} ^{eq}(C))$ . From the previous section, we know that $\operatorname {stp} (a/C)$ has a unique extension to a global $\operatorname {acl} ^{eq}(C)$ -invariant type. By a slight abuse of notation, denote this $\operatorname {stp} (a/C)|\mathbb {U}$ . We are thus using the symbol $|$ to denote extension, not restriction. Also, if $B$ is any subset of $\mathbb {U} ^{eq}$ , we let $\operatorname {stp} (a/C)|B$ denote the restriction of $\operatorname {stp} (a/C)|\mathbb {U}$ to $B$ .

Fix some small base set $C$ . Let $C'=\operatorname {acl} ^{eq}(C)$ . If $a$ and $b$ are (possibly infinite) tuples, let $a\downarrow _{C}b$ indicate that there exist global $C'$ -definable types $p$ and $q$ such that $(a,b)\models (p\otimes q)|C'$ . Then $a\models p|C'$ and $b\models q|C'$ . Since types over $C'$ have unique $C'$ -definable extensions, $p$ must be $\operatorname {tp} (a/C')|\mathbb {U}$ , $q$ must be $\operatorname {tp} (b/C')|\mathbb {U}$ , and $p\otimes q$ must be $\operatorname {tp} (ab/C')|\mathbb {U}$ . So $a\downarrow _{C}b\iff (\operatorname {stp} (a/C)|\mathbb {U} )\otimes (\operatorname {stp} (b/C)|\mathbb {U} )=\operatorname {stp} (ab/C)|\mathbb {U} .$

If $p=\operatorname {stp} (a/C)|\mathbb {U}$ and $q=\operatorname {stp} (b/C)|\mathbb {U}$ , then $a\downarrow _{C}b$ is equivalent to $\operatorname {stp} (ab/C)|\mathbb {U} =p\otimes q$ . Because types over $C'$ are in bijective correspondence with global $C'$ -definable types, this is equivalent to $ab\models p\otimes q|C'$ . From the definition of $p\otimes q$ , this is the same as saying that

$b\models q|C'$
$a\models p|C'b$ .

But (1) is automatic, since $q=\operatorname {tp} (b/C')|\mathbb {U}$ . So $a\downarrow _{C}b$ is equivalent to $a\models p|C'b$ , or equivalently, $a\models \operatorname {tp} (a/C')|C'b$ .

At this point, we have at least two equivalent definitions for $a\downarrow _{C}b$ :

$(a,b)\models p\otimes q|C'$ for some $C'$ -definable types $p$ and $q$ .
$a\models \operatorname {stp} (a/C)|C'b$ .

where $C'=\operatorname {acl} ^{eq}(C)$ .

Lemma.

(a): $a\downarrow _{C}b\iff b\downarrow _{C}a$ . This fact is called symmetry.
(b): $a\downarrow _{C}b$ depends only on the underlying sets of $a$ and $b$ , and not on the orderings of the tuples $a$ and $b$ . So $\downarrow$ is really a relation on sets, not tuples.
(c): If $A'\subseteq A$ and $B'\subseteq B$ , then $A\downarrow _{C}B$ implies $A'\downarrow _{C}B'$ . This fact is called monotonicity.
(d): $A\downarrow _{C}B$ holds if and only if $A'\downarrow _{C}B'$ holds for all finite subsets $A'$ of $A$ and $B'$ of $B$ . This fact is called finite character.
(e): If $A\downarrow _{C}B$ and $D$ is another set, then we can find $A'\equiv _{BC}A$ such that $A'\downarrow _{C}BD$ . This is called right extension.
(f): If $\sigma$ is an automorphism of $\mathbb {U}$ , then $A\downarrow _{C}B\iff \sigma (A)\downarrow _{\sigma (C)}\sigma (B)$ . This is called automorphism invariance. Equivalently, if $A'B'C'\equiv _{\emptyset }ABC$ , then $A\downarrow _{C}B\iff A'\downarrow _{C'}B'$ .
(g): If $A\downarrow _{C}B$ , then $A\downarrow _{C}\operatorname {acl} ^{eq}(BC)$ .

Proof.

(a): This comes from Theorem 2 above, and the first definition of $\downarrow$ .
(b): The fact that $a\downarrow _{C}b$ depends only on $b$ as a set, not as a tuple, is clear from the second of the two definitions of $\downarrow$ given above. Then by symmetry, it only depends on $a$ as a set.
(c): If $a\downarrow _{C}B$ holds and $B'\subset B$ , then $a$ realizes $p|C'B$ , where $p=\operatorname {tp} (a/C')|\mathbb {U}$ . Clearly the tuple $a$ also realizes the smaller type $p|C'B'$ , so $a\downarrow _{C}B'$ . This gives monotonicity on the right: $A\downarrow _{C}B\implies A\downarrow _{C}B'$ if $B'\subset B$ . By symmetry we also get monotonicity on the left.
(d): By symmetry, it suffices to show that $a\downarrow _{C}B$ holds if and only if $a\downarrow _{C}B'$ holds for all finite subsets $B'\subset B$ . Let $p=\operatorname {tp} (a/C')|\mathbb {U}$ . By the second definition of $\downarrow$ , $a\downarrow _{C}B'$ is equivalent to $a\models p|C'B'$ for all $B'$ . But $a$ realizes $p|C'B$ if and only if $a$ realizes the restriction of that type to all finite subsets. So $a$ realizes $p|C'B$ if and only if $a$ realizes $p|C'B'$ for all finite $B'\subset B$ .
(e): Suppose $a\downarrow _{C}B$ and $D$ is some set. Let $p=\operatorname {tp} (a/C')|\mathbb {U}$ . Let $a'$ realizes $p|C'BD$ . Then $\operatorname {tp} (a'/C')=\operatorname {tp} (a/C')$ , so $p$ is also $\operatorname {tp} (a'/C')|\mathbb {U}$ . Therefore $a'\downarrow _{C}BD$ is equivalent to $a'\models p|C'BD$ , which is true. To see that $a'\equiv _{BC}a$ , note that because $a\downarrow _{C}B$ , we know that $a$ realizes $p|C'B$ . Thus $a'$ and $a$ both realize $p|CB$ , and therefore $a\equiv _{BC}a'$ .
(f): This is clear from the definitions, which broke no symmetries of the monster.
(g): By right extension, we can find $A'\equiv _{BC}A$ such that $A'\downarrow _{C}\operatorname {acl} ^{eq}(BC)$ . Let $\sigma$ be an automorphism fixing $BC$ and sending $A'$ back to $A$ . By automorphism invariance, $A\downarrow _{C}\sigma (\operatorname {acl} ^{eq}(BC))$ . But $\sigma$ fixes $BC$ , so it can at most permute the members of $\operatorname {acl} ^{eq}(BC)$ . In particular, $\sigma (\operatorname {acl} ^{eq}(BC))$ is the same underlying set as $\operatorname {acl} ^{eq}(BC)$ , so by part (a), $A\downarrow _{C}\operatorname {acl} ^{eq}(BC)$ .

QED

By monotonicity and part (g), we have the following equivalence $A\downarrow _{C}B\iff A\downarrow _{C}\operatorname {acl} ^{eq}(BC).$ By the second definition of $\downarrow$ , we conclude $A\downarrow _{C}B\iff A\models p|\operatorname {acl} ^{eq}(BC),$ where $p$ is $\operatorname {stp} (A/C)|\mathbb {U}$ . The type $p$ is $\operatorname {acl} ^{eq}(C)$ -definable, hence $\operatorname {acl} ^{eq}(BC)$ -definable. By stability, types over $\operatorname {acl} ^{eq}(BC)$ have unique global $\operatorname {acl} ^{eq}(BC)$ -definable extensions, so $A\models p|\operatorname {acl} ^{eq}(BC)$ is equivalent to $\operatorname {stp} (A/BC)|\mathbb {U} =p$ .

In summary, $A\downarrow _{C}B$ is equivalent to the following: $\operatorname {stp} (A/C)|\mathbb {U} =\operatorname {stp} (A/BC)|\mathbb {U} .$ This gives a third definition of $\downarrow$ .

Lemma. Suppose $C_{1}\subset C_{2}\subset C_{3}$ and $A$ is a set. Then $A\downarrow _{C_{1}}C_{3}$ if and only if $A\downarrow _{C_{1}}C_{2}$ and $A\downarrow _{C_{2}}C_{3}$ . This fact is called transitivity.

Proof. First suppose that $A\downarrow _{C_{1}}C_{2}$ and $A\downarrow _{C_{2}}C_{3}$ . By the third definition of $\downarrow$ , we see that $\operatorname {stp} (A/C_{1})|\mathbb {U} =\operatorname {stp} (A/C_{2})|\mathbb {U} =\operatorname {stp} (A/C_{3})|\mathbb {U} .$ By transitivity of equality, $\operatorname {stp} (A/C_{1})|\mathbb {U} =\operatorname {stp} (A/C_{3})|\mathbb {U}$ , which means $A\downarrow _{C_{1}}C_{3}$ by the third definition of $\downarrow$ .

Conversely, suppose that $A\downarrow _{C_{1}}C_{3}$ . By right monotonicity, $A\downarrow _{C_{1}}C_{2}$ . Then $\operatorname {stp} (A/C_{3})|\mathbb {U} =\operatorname {stp} (A/C_{1})|\mathbb {U} =\operatorname {stp} (A/C_{2})|\mathbb {U} .$ By transitivity of equality, $\operatorname {stp} (A/C_{2})|\mathbb {U} =\operatorname {stp} (A/C_{3})|\mathbb {U}$ , which means $A\downarrow _{C_{2}}C_{3}$ by the third definition of $\downarrow$ . QED

We now prove the remaining essential facts for the forking calculus:

Lemma.

(1): $A\downarrow _{B}B$ always holds.
(2): $A\downarrow _{B}A$ holds if and only if $A\subset \operatorname {acl} ^{eq}(B)$ .
(3): Suppose $C=\operatorname {acl} ^{eq}(C)$ , or more generally, $\operatorname {acl} ^{eq}(C)=\operatorname {dcl} ^{eq}(C)$ . (In particular, this holds if $C$ is a model). If $A\downarrow _{C}B$ and $A'\downarrow _{C}B$ , then $A'\equiv _{C}A$ implies $A'\equiv _{BC}A$ .
(4): There is some cardinal $\kappa =\kappa (T)$ such that if $a$ is a finite tuple and $C$ is a small set, then there exists $C'\subset C$ with $|C'|\leq \kappa$ and $a\downarrow _{C'}C$ . This is called local character.

Proof.

(1): By the third definition of $\downarrow$ , this amounts to showing that $\operatorname {stp} (A/B)|\mathbb {U}$ equals itself.
(2): Suppose $A\subset \operatorname {acl} ^{eq}(B)$ . By (1), $A\downarrow _{B}B$ . By the lemma above, $A\downarrow _{B}\operatorname {acl} ^{eq}(AB)$ . But $A\subset \operatorname {acl} ^{eq}(AB)$ , so by monotonicity on the right, $A\downarrow _{B}A$ . Conversely, suppose $A\downarrow _{B}A$ . We want to show that $A\subset \operatorname {acl} ^{eq}(B)$ . By finite character, we may assume that $A$ is a finite tuple $a$ . Now $\operatorname {stp} (a/B)|\mathbb {U} =\operatorname {stp} (a/Ba)|\mathbb {U}$ . But the constant type $x=a$ is clearly the unique $Ba$ -definable type extending $\operatorname {stp} (a/Ba)$ , so $\operatorname {stp} (a/B)|\mathbb {U}$ must be the constant type $x=a$ . In order for this to be $\operatorname {acl} ^{eq}(B)$ -invariant, the element $a$ must be fixed by every automorphism fixing $\operatorname {acl} ^{eq}(B)$ . This forces $a$ to be in $\operatorname {acl} ^{eq}(B)$ .
(3): Suppose $A\downarrow _{C}B$ and $A'\downarrow _{C}B$ and $A'\equiv _{C}A$ . Because $C$ is algebraically closed, strong types over $C$ are the same as types over $C$ . So $\operatorname {stp} (A/BC)|\mathbb {U} =\operatorname {tp} (A/C)|\mathbb {U} =\operatorname {tp} (A'/C)|\mathbb {U} =\operatorname {stp} (A'/BC)|\mathbb {U} .$ This ensures that $\operatorname {stp} (A/BC)=\operatorname {stp} (A'/BC)$ , so in particular $\operatorname {tp} (A/BC)=\operatorname {tp} (A'/BC)$ .
(4): We can take $\kappa$ to be $|T|$ . Let $p=\operatorname {stp} (a/C)|\mathbb {U}$ . Then $p$ is $\operatorname {acl} ^{eq}(C)$ -definable. The definition of $p$ consists in a map assigning to each formula $\phi$ an $\operatorname {acl} ^{eq}(C)$ -formula $d_{p}\phi$ . There are only $|T|$ formulas $\phi$ , so there must be some subset $C'\subset C$ of size at most $|T|$ such that $d_{p}\phi$ is over $\operatorname {acl} ^{eq}(C')$ for every $\phi$ . Thus $p$ is $\operatorname {acl} ^{eq}(C')$ -definable. Now $\operatorname {stp} (a/C')$ is a restriction of $\operatorname {stp} (a/C)$ which is a restriction of $p$ . Since $p$ is $\operatorname {acl} ^{eq}(C')$ -definable, $p$ must in fact be $\operatorname {stp} (a/C')|\mathbb {U}$ . Then $\operatorname {stp} (a/C')|\mathbb {U} =p=\operatorname {stp} (a/C)|\mathbb {U}$ , so $a\downarrow _{C'}C$ .

QED

Suppose $B\subset B'$ are two small sets, and $p$ is a type over $B$ . Let $p'$ be an extension of $p$ to $B'$ . We say that $p'$ is a non-forking extension of $p$ , or that $p'$ does not fork over $B$ , if $a\downarrow _{B}B'$ for any realization $a$ of $p'$ . The choice of $a$ does not matter, by automorphism invariance. ::: ::: :::