If is a small set of parameters, a set of -indiscernible sequences is said to be mutually indiscernible if each sequence in the set is indiscernible over the union of and the other indiscernible sequences. For example, and are mutually indiscernible if is an indiscernible sequence over , and is an indiscernible sequence over .
Mutually indiscernible sequences can be stretched, extended, and extracted just like indiscernible sequences. For example, for two sequences, one has the following
Let and be two sequences, and let be a set of parameters. Then, passing to an elementary extension if necessary, there exist sequences and , mutually indiscernible over , that are related to the original sequences in the following way: if a formula holds for some , and some , then there exist and such that holds.
For example, if the lived in a sort with a partial ordering, and if , then will hold. If held for every , then will hold for every .
This theorem doesn't seem to follow directly from Ramsey's theorem, but can be proven using Morley sequences of global invariant types in the same way that Ramsey's theorem can be proven. One uses the following fact: if and are two global -invariant types, and realizes , then and will be mutually indiscernible over .
(If somebody knows a direct proof using Ramsey's theorem, they should add it here.)
The ability to extract mutually indiscernible sequences is an important tool for working with ict and inp patterns. ::: ::: :::