Work in a stable theory with monster model .

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

**Fact.** Let be a type over a set . Let be a formula. Then there is at least one which is consistent with and which has finite orbit under .

If is stable, so is . To see this, let be a formula in . Then and come from sorts of the form and , where and are sorts (or products of sorts) in , and and are definable equivalence relations on and . Let be the natural projection map, and let . Then is (equivalent to) a formula in , so it does not have the order property. If has the order property, then there exist for such that if and only if . Choosing and , we get that if and only if , a contradiction.

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

**Observation 1.** Let be a small algebraically closed set, . Let be a definable set. Suppose has finitely many conjugates under . Then is -definable, and hence has a unique conjugate under .

*Proof.* If is a code for , then has finitely many conjugates over , hence is in . Since is -definable, is -definable. QED

**Lemma.** Let be a small set. Let be a complete type over and let be a formula. Then there is a global -type which is -invariant (i.e., -invariant), and which is consistent with .

*Proof.* By the fact at the beginning of this page, we can find a global -type which is consistent with and has finitely many conjugates over . Now if is the -definition of , that is, for every , then the -definable set has finitely many conjugates over . By Observation 1, must be -definable. So is -invariant. QED

Recall that if and are two formulas, we can find a third formula such that the sets of the form are precisely the sets of the form and . Specifically, we take to be So acts like if the dummy variables and agree, and acts like if they do not agree.

Iterating this, one sees that given , we can find such that the formulas of the form are exactly the formulas of the form for some and . Consequently, given a finite set of formulas , we can find a single formula such that -formulas are the same thing as -formulas, and consequently -types are the same thing as -types.

By the previous lemma, we conclude that if is a finite set of formulas, if , and if is a complete type over , then there is a global -type which is consistent with and -invariant.

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

**Lemma.** Let be a small set. Let be a complete type over . Then there is a global -invariant complete type extending . The type is -definable.

*Proof.* Let be the partial type over asserting that for every formula , and every , Then is consistent. To see this, for each finite set of formulas , let assert that for every and every . Then is the union of the โs as ranges over bigger and bigger sets, so it suffices to see that is consistent for each . But this follows from the fact that there is a global -invariant -type which is consistent with .

So is consistent. If is any complete type extending it, then is -invariant.

By stability, is definable. For each formula , the -definition of is -invariant, hence -definable. So is -definable. QED

In fact, the type is uniquely determined by . To prove this, we will need a preliminary version of the symmetry of forking.

Recall that if and are two global -invariant types (in any theory), there is a well-defined global -invariant type which is characterized by the fact that for any , the following are equivalent:

- .
- and .

**Theorem 2.** Let be a small set of parameters. Let and be two global -definable types. Then .

*Proof.* If not, there is some formula which belongs to but not to . Let be a sequence recursively constructed as follows:

- is a realization of restricted to
- is a realization of restricted to .

So essentially the sequence is a realization of .

If , then , so holds. On the other hand, if , then , so does not hold. Therefore has the order property, a contradiction. QED

**Corollary 3.** Let . Then each complete type over has a unique global -invariant extension.

*Proof.* Let and be two global -invariant types such that . Suppose . Then there is some formula which is in but not in . Let realize and realize . Then holds and does not, so .

Let be a global -invariant type extending . Note that and . By Lemma 2, and . Now depends on only through , so we should in fact have , contradicting .

More precisely, let be an automorphism over moving to . Since , and is fixed by , we get that . As , we get that , or equivalently, . So , 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 -types turn out to be equivalent to finitary -types, because a single formula 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 where the limit ranges over finite subsets of , and denotes the set of complete types over of tuples indexed by .

Suppose is stable, but perhaps does not eliminate imaginaries. If is a small subset of the monster , or of , then denotes the algebraic closure of within .

If is a tuple, the **strong type** of over , denoted is by definition just . From the previous section, we know that has a unique extension to a global -invariant type. By a slight abuse of notation, denote this . We are thus using the symbol to denote *extension*, not *restriction*. Also, if is any subset of , we let denote the restriction of to .

Fix some small base set . Let . If and are (possibly infinite) tuples, let indicate that there exist global -definable types and such that . Then and . Since types over have unique -definable extensions, must be , must be , and must be . So

If and , then is equivalent to . Because types over are in bijective correspondence with global -definable types, this is equivalent to . From the definition of , this is the same as saying that

- .

But (1) is automatic, since . So is equivalent to , or equivalently, .

At this point, we have at least two equivalent definitions for :

- for some -definable types and .
- .

where .

**Lemma.**

- (a)
- . This fact is called
**symmetry**. - (b)
- depends only on the underlying sets of and , and not on the orderings of the tuples and . So is really a relation on
*sets*, not*tuples*. - (c)
- If and , then implies . This fact is called
**monotonicity**. - (d)
- holds if and only if holds for all finite subsets of and of . This fact is called
**finite character**. - (e)
- If and is another set, then we can find such that . This is called
**right extension**. - (f)
- If is an automorphism of , then . This is called
**automorphism invariance**. Equivalently, if , then . - (g)
- If , then .

*Proof.*

- (a)
- This comes from Theorem 2 above, and the first definition of .
- (b)
- The fact that depends only on as a set, not as a tuple, is clear from the second of the two definitions of given above. Then by symmetry, it only depends on as a set.
- (c)
- If holds and , then realizes , where . Clearly the tuple also realizes the smaller type , so . This gives monotonicity on the right: if . By symmetry we also get monotonicity on the left.
- (d)
- By symmetry, it suffices to show that holds if and only if holds for all finite subsets . Let . By the second definition of , is equivalent to for all . But realizes if and only if realizes the restriction of that type to all finite subsets. So realizes if and only if realizes for all finite .
- (e)
- Suppose and is some set. Let . Let realizes . Then , so is also . Therefore is equivalent to , which is true. To see that , note that because , we know that realizes . Thus and both realize , and therefore .
- (f)
- This is clear from the definitions, which broke no symmetries of the monster.
- (g)
- By right extension, we can find such that . Let be an automorphism fixing and sending back to . By automorphism invariance, . But fixes , so it can at most permute the members of .
*In particular*, is the same underlying set as , so by part (a), .

QED

By monotonicity and part (g), we have the following equivalence By the second definition of , we conclude where is . The type is -definable, hence -definable. By stability, types over have unique global -definable extensions, so is equivalent to .

In summary, is equivalent to the following: This gives a third definition of .

**Lemma.** Suppose and is a set. Then if and only if and . This fact is called **transitivity**.

*Proof.* First suppose that and . By the third definition of , we see that By transitivity of equality, , which means by the third definition of .

Conversely, suppose that . By right monotonicity, . Then By transitivity of equality, , which means by the third definition of . QED

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

**Lemma.**

- (1)
- always holds.
- (2)
- holds if and only if .
- (3)
- Suppose , or more generally, . (In particular, this holds if is a model). If and , then implies .
- (4)
- There is some cardinal such that if is a finite tuple and is a small set, then there exists with and . This is called
**local character**.

*Proof.*

- (1)
- By the third definition of , this amounts to showing that equals itself.
- (2)
- Suppose . By (1), . By the lemma above, . But , so by monotonicity on the right, . Conversely, suppose . We want to show that . By finite character, we may assume that is a finite tuple . Now . But the constant type is clearly the unique -definable type extending , so must be the constant type . In order for this to be -invariant, the element must be fixed by every automorphism fixing . This forces to be in .
- (3)
- Suppose and and . Because is algebraically closed, strong types over are the same as types over . So This ensures that , so in particular .
- (4)
- We can take to be . Let . Then is -definable. The definition of consists in a map assigning to each formula an -formula . There are only formulas , so there must be some subset of size at most such that is over for every . Thus is -definable. Now is a restriction of which is a restriction of . Since is -definable, must in fact be . Then , so .

QED

Suppose are two small sets, and is a type over . Let be an extension of to . We say that is a **non-forking extension** of , or that **does not fork over **, if for any realization of . The choice of does not matter, by automorphism invariance. ::: ::: :::