Two tuples and (in the same sort) have the same **strong type** over a set of parameters if holds for every -definable equivalence relation with finitely many equivalence classes. An equivalent condition is that and have the same type over , the set of imaginaries which are algebraic over .

If and have the same strong type over , then they have the same type over , so this is a "stronger" notion than the notion of a type. The strong type of over is sometimes denoted . The set of realizations of is type-definable, and so can be thought of as a partial type over some set.

There are two even stronger notions of "strong type" which appear in certain settings.

Two tuples and have the same **Kim-Pillay strong type** over if holds for every equivalence relation which is type-definable over and has a *bounded* number of equivalence classes. Here, "bounded" means that the number of equivalence classes does not grow in elementary extensions, or is small compared to the size of the monster. The equivalence relation of having the same Kim-Pillay strong type is the unique smallest bounded equivalence relation which is type-definable over .

As in the case of strong type, the set of realizations of the Kim-Pillay strong type of over is type-definable, and so a Kim-Pillay strong type can be thought of as a partial type over some set. In the same way that strong type can be defined more directly using imaginaries, Kim-Pillay strong type can be defined more directly using hyperimaginaries: and have the same Kim-Pillay strong type over if and only if they have the same type over , the set of hyperimaginaries which have bounded number of conjugates over .

Finally, the relation of having the same **Lascar strong type** over is defined to be the minimum -invariant equivalence relation with a bounded number of classes. There are several equivalent definitions:

- If means that for some model containing , then the relation of having the same Lascar strong type over is the transitive closure of .
- Let be the monster. If is the subgroup of generated by for a model containing , then and have the same Lascar strong type over if and only if they are conjugate via . (This is just a restatement of the previous bullet point.)
- If means that there is a -indiscernible sequence whose first two terms are and , then the relation of having the same Lascar strong type over is the transitive closure of .

A theory is called -compact if the relation of having the same Lascar strong type over is type-definable for every . Equivalently, Kim-Pillay type and Lascar strong type agree. Simple theories are known to be -compact.

For stable theories, something even better happens: strong type, Kim-Pillay strong type, and Lascar strong type all agree. This also happens for o-minimal and c-minimal theories, by a result in Hrushovski and Pillay’s paper *On NIP and Invariant Measures*.

Let be the ambient monster model.

The two definitions of strong type are equivalent.

*Proof.* Suppose that holds for every -definable equivalence relation with finitely many equivalence classes. To show that , it suffices to show that for every -definable set , . But if is -definable, then the code for is in , hence has finitely many conjugates over . Let be the equivalence relation such that if and only if for every conjugate of over . If has conjugates over , then has at most equivalence classes. The equivalence classes of are boolean combinations of definable sets, so is definable. Since is clearly -invariant, is -definable. Hence holds. Therefore .

Conversely, suppose and have the same type over . Let be a -definable equivalence relation with finitely many equivalence classes. If is an equivalence class of and , then is an equivalence class of . Since has finitely many classes, there are finitely many possibilities for , so the code for is in . Therefore, is -definable, and . As was an arbitrary equivalence class of , it follows that . QED

If and have the same strong type over , then they have the same type over .

*Proof.* If is a -definable set, then we need to show that . Let be the equivalence relation with two classes, and the complement of . Then is -definable with finitely many classes, so . QED

There is a minimum equivalence relation which is type-definable over and has a bounded number of equivalence classes. (So the definition of Kim-Pillay strong type makes sense.)

*Proof.* If is a small family of equivalence relations which are type-definable over , then is also an equivalence relation which is type-definable over . Moreover, if each is bounded (i.e., has a bounded number of equivalence classes), then so is the equivalence relation . Take to be the class of all bounded equivalence relations which are type-definable over . QED

Similarly, one proves that there is a minimum equivalence relation which is bounded and -invariant. (If is -invariant, then whether holds depends only on . There are a bounded number of possibilities for , so there are a bounded number of -invariant equivalence relations.)

Fix . Let mean that there is some model such that . Let indicate that there is some -indiscernible sequence beginning with . Then and have the same transitive closure.

*Proof.* Suppose that holds. Then holds for some model containing . Let be a global *M*-invariant type extending . Let be a Morley sequence for over , so , , , and so on. Then and are both indiscernible sequences over . So and . So is in the transitive closure of . (Technically speaking, we should also show that is symmetric. This follows from the fact that if is an indiscernible sequence, then we can extend this sequence to the left, reverse it, and throw away the terms preceding .)

Conversely, suppose that holds. Then there is a -indiscernible sequence whose first two terms are and . Let be a model containing . Let be an -indiscernible sequence extracted from . Then and have the same type over , so we can find some such that . As , is a model containing . As and is -indiscernible, is -indiscernible. Thus all elements of have the same type over . In particular, . So . QED

The transitive closure of is a bounded equivalence relation.

*Proof.* Let be some model containing . Then any two elements having the same type over are equivalent with respect to the transitive closure of . So the transitive closure of has no more equivalence classes than there are types over . QED

If is a -invariant bounded equivalence relation, and , then .

*Proof.* By definition of , we can find some -indiscernible sequence such that and . Extend the sequence to be longer than the number of equivalence classes of . Suppose doesn’t hold. By -indiscernibility of the sequence, and -invariance of , we see that fails to hold for any . So each element of the indiscernible sequence is in a different equivalence class, contradicting the choice of the length of the indiscernible sequence. QED

So the transitive closure of is contained in any -invariant bounded equivalence relation, and is therefore the unique minimum -invariant bounded equivalence relation. Consequently, the transitive closure of agrees with the transitive closure of agrees with unique minimum -invariant bounded equivalence relation. So the definitions of Lascar strong type given above agree.

... ::: ::: :::