Two tuples {\displaystyle a} and {\displaystyle b} (in the same sort) have the same strong type over a set of parameters {\displaystyle C} if {\displaystyle aEb} holds for every {\displaystyle C}-definable equivalence relation with finitely many equivalence classes. An equivalent condition is that {\displaystyle a} and {\displaystyle b} have the same type over {\displaystyle \operatorname {acl} ^{eq}(C)}, the set of imaginaries which are algebraic over {\displaystyle C}.

If {\displaystyle a} and {\displaystyle b} have the same strong type over {\displaystyle C}, then they have the same type over {\displaystyle C}, so this is a "stronger" notion than the notion of a type. The strong type of {\displaystyle a} over {\displaystyle C} is sometimes denoted {\displaystyle \operatorname {stp} (a/C)}. The set of realizations of {\displaystyle \operatorname {stp} (a/C)} 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 {\displaystyle a} and {\displaystyle b} have the same Kim-Pillay strong type over {\displaystyle C} if {\displaystyle aEb} holds for every equivalence relation {\displaystyle E} which is type-definable over {\displaystyle C} 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 {\displaystyle C}.

As in the case of strong type, the set of realizations of the Kim-Pillay strong type of {\displaystyle a} over {\displaystyle C} 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: {\displaystyle a} and {\displaystyle b} have the same Kim-Pillay strong type over {\displaystyle C} if and only if they have the same type over {\displaystyle bdd(C)}, the set of hyperimaginaries which have bounded number of conjugates over {\displaystyle C}.

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

A theory is called {\displaystyle G}-compact if the relation of having the same Lascar strong type over {\displaystyle C} is type-definable for every {\displaystyle C}. Equivalently, Kim-Pillay type and Lascar strong type agree. Simple theories are known to be {\displaystyle G}-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.

Proofs of Claims Made Above[]

Let {\displaystyle \mathbb {U} } be the ambient monster model.

The two definitions of strong type are equivalent.

Proof. Suppose that {\displaystyle aEb} holds for every {\displaystyle C}-definable equivalence relation with finitely many equivalence classes. To show that {\displaystyle \operatorname {tp} (a/\operatorname {acl} ^{eq}(C))=\operatorname {tp} (b/\operatorname {acl} ^{eq}(C))}, it suffices to show that for every {\displaystyle \operatorname {acl} ^{eq}(C)}-definable set {\displaystyle D}, {\displaystyle a\in D\iff b\in D}. But if {\displaystyle D} is {\displaystyle \operatorname {acl} ^{eq}(C)}-definable, then the code for {\displaystyle D} is in {\displaystyle \operatorname {acl} ^{eq}(C)}, hence has finitely many conjugates over {\displaystyle C}. Let {\displaystyle E} be the equivalence relation such that {\displaystyle xEy} if and only if {\displaystyle x\in D'\iff y\in D'} for every conjugate {\displaystyle D'} of {\displaystyle D} over {\displaystyle C}. If {\displaystyle D} has {\displaystyle n} conjugates over {\displaystyle C}, then {\displaystyle E} has at most {\displaystyle 2^{n}} equivalence classes. The equivalence classes of {\displaystyle E} are boolean combinations of definable sets, so {\displaystyle E} is definable. Since {\displaystyle E} is clearly {\displaystyle C}-invariant, {\displaystyle E} is {\displaystyle C}-definable. Hence {\displaystyle aEb} holds. Therefore {\displaystyle a\in D\iff b\in D}.

Conversely, suppose {\displaystyle a} and {\displaystyle b} have the same type over {\displaystyle \operatorname {acl} ^{eq}(C)}. Let {\displaystyle E} be a {\displaystyle C}-definable equivalence relation with finitely many equivalence classes. If {\displaystyle D} is an equivalence class of {\displaystyle E} and {\displaystyle \sigma \in \operatorname {Aut} (\mathbb {U} /C)}, then {\displaystyle \sigma (D)} is an equivalence class of {\displaystyle \sigma (E)=E}. Since {\displaystyle E} has finitely many classes, there are finitely many possibilities for {\displaystyle \sigma (D)}, so the code for {\displaystyle D} is in {\displaystyle \operatorname {acl} ^{eq}(C)}. Therefore, {\displaystyle D} is {\displaystyle \operatorname {acl} ^{eq}(C)}-definable, and {\displaystyle a\in D\iff b\in D}. As {\displaystyle D} was an arbitrary equivalence class of {\displaystyle E}, it follows that {\displaystyle aEb}. QED

If {\displaystyle a} and {\displaystyle b} have the same strong type over {\displaystyle C}, then they have the same type over {\displaystyle C}.

Proof. If {\displaystyle D} is a {\displaystyle C}-definable set, then we need to show that {\displaystyle a\in D\iff b\in D}. Let {\displaystyle E} be the equivalence relation with two classes, {\displaystyle D} and the complement of {\displaystyle D}. Then {\displaystyle E} is {\displaystyle C}-definable with finitely many classes, so {\displaystyle aEb}. QED

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

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

Similarly, one proves that there is a minimum equivalence relation {\displaystyle E} which is bounded and {\displaystyle C}-invariant. (If {\displaystyle E} is {\displaystyle C}-invariant, then whether {\displaystyle aEb} holds depends only on {\displaystyle \operatorname {tp} (ab/C)}. There are a bounded number of possibilities for {\displaystyle \operatorname {tp} (ab/C)}, so there are a bounded number of {\displaystyle C}-invariant equivalence relations.)

Fix {\displaystyle C}. Let {\displaystyle x\sim y} mean that there is some model {\displaystyle M\supseteq C} such that {\displaystyle x\equiv _{M}y}. Let {\displaystyle x\sim 'y} indicate that there is some {\displaystyle C}-indiscernible sequence beginning with {\displaystyle x,y,\ldots }. Then {\displaystyle \sim } and {\displaystyle \sim '} have the same transitive closure.

Proof. Suppose that {\displaystyle x\sim y} holds. Then {\displaystyle x\equiv _{M}y} holds for some model {\displaystyle M} containing {\displaystyle C}. Let {\displaystyle p} be a global M-invariant type extending {\displaystyle \operatorname {tp} (x/M)=\operatorname {tp} (y/M)}. Let {\displaystyle z_{1},z_{2},\ldots } be a Morley sequence for {\displaystyle p} over {\displaystyle Mxy}, so {\displaystyle z_{1}\models p|Mxy}, {\displaystyle z_{2}\models p|Mxyz_{1}}, {\displaystyle z_{3}\models p|Mxyz_{1}z_{2}}, and so on. Then {\displaystyle x,z_{1},z_{2},\ldots } and {\displaystyle y,z_{1},z_{2},\ldots } are both indiscernible sequences over {\displaystyle M}. So {\displaystyle x\sim 'z_{1}} and {\displaystyle y\sim 'z_{1}}. So {\displaystyle \sim } is in the transitive closure of {\displaystyle \sim '}. (Technically speaking, we should also show that {\displaystyle \sim '} is symmetric. This follows from the fact that if {\displaystyle x,y,\ldots } is an indiscernible sequence, then we can extend this sequence to the left, reverse it, and throw away the terms preceding {\displaystyle y,x,\ldots }.)

Conversely, suppose that {\displaystyle x\sim 'y} holds. Then there is a {\displaystyle C}-indiscernible sequence {\displaystyle I} whose first two terms are {\displaystyle x} and {\displaystyle y}. Let {\displaystyle M_{0}} be a model containing {\displaystyle C}. Let {\displaystyle I'} be an {\displaystyle M_{0}}-indiscernible sequence extracted from {\displaystyle I}. Then {\displaystyle I'} and {\displaystyle I} have the same type over {\displaystyle C}, so we can find some {\displaystyle M} such that {\displaystyle MI\equiv _{C}M_{0}I'}. As {\displaystyle M\equiv _{C}M_{0}}, {\displaystyle M} is a model containing {\displaystyle C}. As {\displaystyle MI\equiv _{\emptyset }M_{0}I'} and {\displaystyle I'} is {\displaystyle M_{0}}-indiscernible, {\displaystyle I} is {\displaystyle M}-indiscernible. Thus all elements of {\displaystyle I} have the same type over {\displaystyle M}. In particular, {\displaystyle x\equiv _{M}y}. So {\displaystyle x\sim y}. QED

The transitive closure of {\displaystyle \sim } is a bounded equivalence relation.

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

If {\displaystyle E} is a {\displaystyle C}-invariant bounded equivalence relation, and {\displaystyle a\sim 'b}, then {\displaystyle aEb}.

Proof. By definition of {\displaystyle \sim '}, we can find some {\displaystyle C}-indiscernible sequence {\displaystyle a_{1},a_{2},\ldots } such that {\displaystyle a_{1}=a} and {\displaystyle a_{2}=b}. Extend the sequence to be longer than the number of equivalence classes of {\displaystyle E}. Suppose {\displaystyle a_{1}Ea_{2}} doesn’t hold. By {\displaystyle C}-indiscernibility of the sequence, and {\displaystyle C}-invariance of {\displaystyle E}, we see that {\displaystyle a_{i}Ea_{j}} fails to hold for any {\displaystyle i<j}. 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 {\displaystyle \sim '} is contained in any {\displaystyle C}-invariant bounded equivalence relation, and is therefore the unique minimum {\displaystyle C}-invariant bounded equivalence relation. Consequently, the transitive closure of {\displaystyle \sim } agrees with the transitive closure of {\displaystyle \sim '} agrees with unique minimum {\displaystyle C}-invariant bounded equivalence relation. So the definitions of Lascar strong type given above agree.

Examples[]

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