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. ::: ::: :::