A global invariant type is a type over the monster M which does not split over a small set A, or equivalently, is Aut(M/A)-invariant. We say that this global type is "A-invariant" (or "invariant over A") when we want to specify the set A.

In other words, suppose M is a structure, AM is a subset, and suppose that M is |A|+-saturated and |A|+-strongly homogeneous. Then we are interested in (complete) types p(x) on M with the following property: for every {\displaystyle a} from {\displaystyle M} and formula {\displaystyle \phi (x;y)}, whether or not {\displaystyle \phi (x;a)\in p(x)} depends only on {\displaystyle {\text{tp}}(a/A)} (and on {\displaystyle \phi (x;y)}). Equivalently, whenever {\displaystyle a\equiv _{A}b}, we have

{\displaystyle \phi (x;a)\in p(x)\iff \phi (x;b)\in p(x)}

By strong homogeneity, the set of {\displaystyle b} such that {\displaystyle b\equiv _{A}a} is exactly the orbit of {\displaystyle a} under the automorphism group Aut(M/A). So an equivalent condition is that for every a, every formula {\displaystyle \phi (x;y)}, and every {\displaystyle \sigma \in {\text{Aut}}(M/A)}, we have

{\displaystyle \phi (x;a)\in p(x)\iff \phi (x;\sigma (a))\in p(x)}.

This is in turn equivalent to the condition that {\displaystyle p=\sigma ^{*}p} for every {\displaystyle \sigma \in {\text{Aut}}(M/A)}, i.e., that {\displaystyle p} is invariant under Aut(M/A).

Global invariant types are essentially the same thing as what Poizat calls "special sons" in his Course in Model Theory.

A somewhat prototypical example of a global invariant type is the generic type of a geometrically irreducible variety in ACF. Let K be a field, and embed K in some very saturated and strongly homogeneous monster model M of ACF. If {\displaystyle V\subset \mathbb {A} _{K}^{n}} is a geometrically irreducible affine variety, then {\displaystyle V} is irreducible over M, and we can talk about the generic type p(x) ∈ Sn(M). This is the type which says that the n-tuple x lies on V, but not on any strictly smaller M-definable closed subvarieties of V. This type is K-invariant, i.e., Aut(M/K)-invariant. This is fairly clear by symmetry considerations: if {\displaystyle \sigma \in {\text{Aut}}(M/K)}, then {\displaystyle \sigma } sends the variety V to itself, and sends proper subvarieties of V to proper subvarieties of V. Since {\displaystyle p} is characterized as being the unique type over M which lies on V but not on any proper subvarieties, {\displaystyle \sigma (p)} must be the same type as {\displaystyle p}.

We should also point out that coheirs are invariant types: if a global type {\displaystyle p(x)} is a coheir of its restriction to a small model M, then {\displaystyle p(x)} is M-invariant.

Definable types are another source of global invariant types. (In fact, in stable theories, definable types and invariant types are the same thing.)

Existence of global invariant types[]

Work inside a monster model {\displaystyle {\mathfrak {M}}} of some theory.

Theorem: Let M be a small model (i.e., small elementary substructure of {\displaystyle {\mathfrak {M}}}), and p(x) be a complete type over M. Then there is at least one global M-invariant type extending p.

Proof: Let {\displaystyle \Sigma (x)} be the (big) partial type over {\displaystyle {\mathfrak {M}}} consisting of the statements

{\displaystyle \phi (x;a)\leftrightarrow \phi (x;b)}

for every formula {\displaystyle \phi (x;y)}, and every {\displaystyle a,b} from {\displaystyle {\mathfrak {M}}} such that {\displaystyle a\equiv _{M}b} (i.e., such that a and b have the same type over M).

Note that {\displaystyle \Sigma (x)} is satisfied by every element of M. Indeed, if cM and {\displaystyle a\equiv _{M}b}, then {\displaystyle a\equiv _{c}b} so {\displaystyle ca\equiv _{\emptyset }cb}, and therefore

{\displaystyle {\mathfrak {M}}\models \phi (c;a)\iff {\mathfrak {M}}\models \phi (c;b)}

for every formula {\displaystyle \phi (x;y)}.

Now any finite subset {\displaystyle p_{0}(x)\subset p(x)} is satisfied by some tuple c from M. This tuple satisfies {\displaystyle p_{0}(x)\cup \Sigma (x)}. It follows that {\displaystyle p_{0}(x)\cup \Sigma (x)} is consistent for every finite subset {\displaystyle p_{0}(x)\subset p(x)}. Therefore {\displaystyle p(x)\cup \Sigma (x)} is a consistent partial type over the monster {\displaystyle {\mathfrak {M}}}.

Let {\displaystyle q(x)} be any complete type over the monster {\displaystyle {\mathfrak {M}}} extending {\displaystyle p(x)\subset \Sigma (x)}. Then {\displaystyle q(x)} is our desired global M-invariant type. Indeed, if a and b are two tuples from {\displaystyle {\mathfrak {M}}} having the same type over M, then

{\displaystyle q(x)\vdash \phi (x;a)\leftrightarrow \phi (x;b)}

because {\displaystyle q(x)} extends {\displaystyle \Sigma (x)}. But because {\displaystyle q(x)} is a complete type, it follows that

{\displaystyle \phi (x;a)\in q(x)\iff \phi (x;b)\in q(x)}.

Given that this holds for any formula {\displaystyle \phi (x;y)} and any two tuples {\displaystyle a,b} having the same type over M, it follows that {\displaystyle q(x)} is M-invariant, for reasons explained above.

QED.

From this we see that non-trivial examples of global invariant types exist in any theory.

Invariant types as a variation on Definable types[]

A global type p(x) is A-definable if for every formula {\displaystyle \phi (x;y)}, there is a formula {\displaystyle \psi (y)} over A such that

{\displaystyle \phi (x;b)\in p(x)\iff {\mathfrak {M}}\models \psi (b)},

for every b in M. We think of the map {\displaystyle \phi (x;y)\mapsto \psi (y)} as a "definition schema." The formula {\displaystyle \psi (y)} is called the "{\displaystyle \phi }-definition of p." If p is definable, then it is always A-definable over some small set A.

Now if {\displaystyle b\equiv _{A}b'}, then

{\displaystyle \phi (x;b)\in p(x)\iff \models \psi (b)\iff \models \psi (b')\iff \phi (x;b')\in p(x)},

where the middle {\displaystyle \iff } comes from the fact that {\displaystyle \psi (y)} is a formula over A. Thus p is A-definable; A-definable types are A-invariant. The notion of "A-invariant type" can be seen as a generalization of "A-definable type" in which the {\displaystyle \phi }-definition of p is no longer given by a formula over A, but by a set of complete types over A. That is, there is some subset {\displaystyle X\subset S(A)} such that for every b,

{\displaystyle \phi (x;b)\in p(x)\iff {\text{tp}}(b/A)\in X}.

If {\displaystyle X} were the clopen set associated with some A-formula {\displaystyle \psi (y)}, then this would mean that

{\displaystyle \phi (x;b)\in p(x)\iff \models \psi (b)}.

An A-definable type p(x) over a model M has a unique global extension q(x) which is A-definable. Essentially, the definition schema for q(x) must be the same as the definition schema for p(x). Something similar happens with invariant types:

Theorem: If M is |A|+-saturated and |A|+-strongly homogeneous, then each A-invariant type on M has a unique global extension which is A-invariant.

Proof: Let q(x) be the set of all formulas {\displaystyle \phi (x;b)}, where b is a tuple from the monster {\displaystyle {\mathfrak {M}}} such that {\displaystyle b\equiv _{A}c} for some tuple c from M such that {\displaystyle \phi (x;c)\in p(x)}. We claim that q(x) is a consistent type, it is a complete type over the monster, that it is A-invariant, and that it is the only global A-invariant type.

First of all, we check consistency. Suppose for the sake of contradiction that

{\displaystyle \{\phi _{1}(x;b_{1}),\ldots ,\phi _{n}(x;b_{n})\subset q(x)}

is inconsistent. By definition of q(x), we can find {\displaystyle c_{1},\ldots ,c_{n}} such that {\displaystyle b_{i}\equiv _{A}c_{i}} for each i, and {\displaystyle \phi _{i}(x;c_{i})\in p(x)}.

Now because M is |A|+-saturated, we can find {\displaystyle d_{1},\ldots ,d_{n}} in M such that

{\displaystyle b_{1}b_{2}\cdots b_{n}\equiv _{A}d_{1}d_{2}\cdots d_{n}}.

Then for each i,

{\displaystyle d_{i}\equiv _{A}b_{i}\equiv _{A}c_{i}}.

By strong homogeneity, some {\displaystyle \sigma \in {\text{Aut}}(M/A)} sends {\displaystyle d_{i}} to {\displaystyle c_{i}}. By invariance of p(x),

{\displaystyle \phi _{i}(x;d_{i})\in p(x)\iff \phi _{i}(x;c_{i})\in p(x)}.

So {\displaystyle \phi _{i}(x;d_{i})\in p(x)} for {\displaystyle i=1,\ldots ,n}. Now by assumption

{\displaystyle \models \neg \exists x:\bigwedge _{i=1}^{n}\phi _{i}(x;b_{i})}.

Since the bi's collectively have the same type as the di's,

{\displaystyle \models \neg \exists x:\bigwedge _{i=1}^{n}\phi _{i}(x;d_{i})}.

But we just claimed that {\displaystyle \phi _{i}(x;d_{i})\in p(x)} for each i, so p(x) is inconsistent, contradicting the fact that it is a complete type.

Next, we check that q is a complete type. Let {\displaystyle \phi (x;y)} be a formula and b be a tuple from the monster. By saturation of M, we can find some c in M such that {\displaystyle b\equiv _{A}c}. Because p is complete, either {\displaystyle \phi (x;c)} or {\displaystyle \neg \phi (x;c)} is in p(x). Then by definition of q(x), either {\displaystyle \phi (x;b)} or {\displaystyle \neg \phi (x;b)} is in q(x). So q is complete.

Next we check A-invariance. Suppose {\displaystyle b\equiv _{A}b'} for {\displaystyle b,b'} in the monster. By saturation of M, we can find c in M realizing {\displaystyle {\text{tp}}(b/A)={\text{tp}}(b'/A)}. Then by definition of q, for each formula {\displaystyle \phi (x;y)}

{\displaystyle \phi (x;b)\in q(x)\iff \phi (x;c)\in p(x)\iff \phi (x;b')\in q(x)}.

As explained above, this shows that q is A-invariant.

Finally, suppose r were some other A-invariant global type extending p. Then for any b in the monster and any formula {\displaystyle \phi (x;y)}, we have

{\displaystyle \phi (x;b)\in r(x)\iff \phi (x;c)\in r(x)\iff \phi (x;c)\in p(x)\iff \phi (x;c)\in q(x)\iff \phi (x;b)\in q(x)}

where c is any realization of tp(b/A) in M.

QED.

The tensor product of global invariant types[]

Work in a monster model {\displaystyle {\mathfrak {M}}}. Recall the following (standard) notation:

Lemma: Let A be a small subset, let q(x) be a (complete) type over A, and let p(y) be a global A-invariant type. Then

{\displaystyle S=\{(a,b){\text{ from the monster}}:b\models q{\text{ and }}a\models p\upharpoonright Ab\}}

is the set of realizations (in the monster) of some complete type {\displaystyle r(x;y)} over A.

Proof: First of all, S is non-empty, because q and p are consistent types (and the monster is saturated).

Next, any two tuples in S have the same type over A. Indeed, suppose that {\displaystyle (a,b),(a',b')\in S}. Then {\displaystyle b} and {\displaystyle b'} both realize q, so there exists some automorphism {\displaystyle \sigma } over A sending {\displaystyle b} to {\displaystyle b'}. Because p is A-invariant, {\displaystyle \sigma (p)=p}. The fact that {\displaystyle a} realizes {\displaystyle p\upharpoonright Ab} implies therefore that {\displaystyle \sigma (a)} realizes

{\displaystyle \sigma (p)\upharpoonright A\sigma (b)=p\upharpoonright Ab'={\text{tp}}(a'/Ab')}.

Thus {\displaystyle \sigma (a)\equiv _{Ab'}a'}. But then

{\displaystyle ab\equiv _{A}\sigma (a)\sigma (b)=\sigma (a)b'\equiv _{A}a'b'},

so {\displaystyle (a,b)} and {\displaystyle (a',b')} have the same type over A, as claimed.

Finally, suppose that {\displaystyle (a,b)} is in S, and {\displaystyle a'b'\equiv _{A}ab}. Then {\displaystyle b'\equiv _{A}b}, so {\displaystyle b'} realizes q. Also, there is some automorphism {\displaystyle \sigma } fixing A, and sending {\displaystyle b} to {\displaystyle b'}. Then {\displaystyle \sigma } fixes p, so

{\displaystyle a\models p\upharpoonright Ab\implies \sigma (a)\models p\upharpoonright Ab'}.

Meanwhile,

{\displaystyle a'b'\equiv _{A}ab\equiv _{A}\sigma (a)\sigma (b)=\sigma (a)b'},

so

{\displaystyle a'\equiv _{Ab'}\sigma (a)}.

Then since {\displaystyle \sigma (a)} realizes {\displaystyle p\upharpoonright Ab'}, so does {\displaystyle a'}. Now we know that

{\displaystyle b'\models q} and {\displaystyle a'\models p\upharpoonright Ab'}.

So {\displaystyle (a',b')\in S}, as claimed.

(A shorter way to see this is to argue from symmetry that S must be A-invariant, because it is defined using only A, a type over A, and an A-invariant global type. So any symmetry which fixes A must certainly send S to itself. Then if {\displaystyle (a,b)\in S} and {\displaystyle (a',b')\equiv _{A}(a,b)}, some automorphism over A sends {\displaystyle (a,b)} to {\displaystyle (a',b')}, and therefore {\displaystyle (a',b')} is in S.)

At any rate, we have shown that S is non-empty, any two elements have the same type over A, and that any tuple having the same type over A as someone in S is itself in S. Therefore, S is exactly the set of realizations of some complete type r over A.

QED.

Theorem/Definition: Let p(x) and q(y) be two global A-invariant types. Then there is a unique global type {\displaystyle (p\otimes q)(x,y)} with the following property: for every small set C containing A, and every a and b from the monster, the following are equivalent:

The type {\displaystyle p\otimes q} is A-invariant. Moreover, {\displaystyle p\otimes q} does not depend on the choice of A (i.e., it remains the same if we replace A with a bigger set.)

Proof: Note that for any small C containing A, p is C-invariant, because {\displaystyle {\text{Aut}}({\mathfrak {M}}/C)\subset {\text{Aut}}({\mathfrak {M}}/A)}. By the Lemma, we can find a complete type {\displaystyle r_{C}(x;y)} over C such that the following are equivalent for a and b tuples from the monster of the appropriate lengths:

We claim that if {\displaystyle C\subset D}, then {\displaystyle r_{D}} extends {\displaystyle r_{C}}. Equivalently, if {\displaystyle (a,b)\models r_{D}}, then {\displaystyle (a,b)\models r_{C}}. But this is clear because

{\displaystyle b\models q\upharpoonright D\implies b\models q\upharpoonright C}

and

{\displaystyle a\models p\upharpoonright Da\implies a\models p\upharpoonright Ca}.

Let {\displaystyle p\otimes q} be the union of the {\displaystyle r_{C}}'s as C ranges over small supsersets of A. From what we have just seen, {\displaystyle p\otimes q} is a consistent type, hence a complete global type. It has the desired characterization that for any small set C containing A,

if and only if

This uniquely characterizes the type. Moreover, {\displaystyle p\otimes q} must be A-invariant, by symmetry. (It is defined only using A-invariant entities.)

Finally, let us verify that the choice of A does not matter. For small BA, let {\displaystyle p\otimes _{B}q} denote the B-invariant tensor product of {\displaystyle p} and {\displaystyle q} viewed as B-invariant types. The conditions which uniquely characterize {\displaystyle p\otimes _{A}q} are clearly as strong as the conditions which uniquely characterize {\displaystyle p\otimes _{B}q}, so the two must be equal:

{\displaystyle p\otimes _{A}q=p\otimes _{B}q}.

Now if A and B are two different small sets over which p and q are invariant, then

{\displaystyle p\otimes _{A}q=p\otimes _{A\cup B}q=p\otimes _{B}q}.

QED.

Now if {\displaystyle p(x)} and {\displaystyle q(y)} are two invariant types (over some small sets), then we can uniquely define the tensor product {\displaystyle (p\otimes q)(x,y)}, by finding some A over which both p and q are invariant. (For example, if p is B-invariant and q is C-invariant, then any small ABC works.)

The tensor product {\displaystyle (p\otimes q)(x,y)} is usually denoted {\displaystyle p(x)\otimes q(y)}.

The Example of ACF[]

The tensor product operation on global invariant types generalizes the notion of taking the cartesian product of two varieties, in the following sense. Work in a monster model of ACF. Let V and W be two irreducible affine varieties, and let p and q denote the corresponding generic types, over the monster model. Then {\displaystyle p\otimes q} is the generic type of {\displaystyle V\times W}. Let's prove this.

Claim: Let V be an irreducible variety. Let p be the global generic type of V. Let K be any (small) field over which V is defined. Then a tuple a (from the monster) realizes {\displaystyle p\upharpoonright K} if and only if a is on V and tr.deg(a/K) = dim(V).

Proof: First suppose that {\displaystyle a\models p\upharpoonright K}. The statement {\displaystyle x\in V} is certainly a formula over K, so it is in {\displaystyle p\upharpoonright K}, and therefore {\displaystyle a\in V}. This ensures that tr.deg(a/K) ≤ dim(V). If the equality was strict, then a would lie on some K-definable variety W of dimension less than dim(V). (Of course W might not be irreducible.) Then VW is a K-definable proper closed subvariety of V. The type p(x) certainly contains the statement xVW, and since this statement is over K, it is in {\displaystyle p\upharpoonright K}. Therefore aVW, a contradiction.

For the converse, let {\displaystyle {\overline {K}}} denote the algebraic closure of {\displaystyle K}. This is a model of ACF, so an elementary substructure of the monster (by model completeness of ACF). The type {\displaystyle p(x)\upharpoonright {\overline {K}}} says (among other things) that x is on V and not on any strictly smaller {\displaystyle {\overline {K}}}-definable subvarieties of V, if not more. But by the characterization of complete types over models of ACF, {\displaystyle p\upharpoonright {\overline {K}}} can be nothing but the generic type of V, as one would expect.

Now if a is on V and tr.deg(a/K) = dim(V), then a is on V, and not on any strictly smaller {\displaystyle {\overline {K}}}-definable subvarieties of V. (Indeed, if a is on {\displaystyle {\overline {K}}}-definable {\displaystyle W\subsetneq V}, then dim(W) < dim(V) and

{\displaystyle {\text{tr.deg}}(a/K)={\text{tr.deg}}(a/{\overline {K}})\leq {\text{dim}}(W)<{\text{dim}}(V)={\text{tr.deg}}(a/K)},

a contradiction.) So a realizes the generic type of V over {\displaystyle {\overline {K}}}, i.e., a realizes {\displaystyle p\upharpoonright {\overline {K}}}. It certainly then also realizes the restriction of this to K, which is {\displaystyle p\upharpoonright K}.

The claim is proven.

Theorem: Let V and W be irreducible varieties with global generic types p(x and q(y). Then {\displaystyle p(x)\otimes q(y)} is the generic type of {\displaystyle V\times W}.

Proof: Let K be a field over which V and W are defined. So p, q, and {\displaystyle p\otimes q} are all K-invariant. Let r be the global generic type of {\displaystyle V\times W}. The type r is also K-invariant.

For any small LK, and tuples a and b of the appropriate lengths, we have the following series of equivalent statements

So we see that {\displaystyle p\otimes q} and {\displaystyle r} have the same restriction to any small subfield. Therefore, they are equal.

QED.

Associativity[]

The tensor-product operation on invariant types is associative, in the sense that {\displaystyle ((p\otimes q)\otimes r)} is the same as {\displaystyle (p\otimes (q\otimes r))}. This follows by unwinding the definitions.

Indeed, if C is any small set over which p, q, and r are invariant, and if a, b, and c are appropriately-sized tuples, then the following conditions are equivalent:

Each of these conditions is equivalent to the next one, by the definition of {\displaystyle \otimes }.

Since associativity holds, we can write {\displaystyle p(x)\otimes q(y)\otimes r(z)} unambiguously.

In general, a realization of {\displaystyle p_{1}(x_{1})\otimes \cdots \otimes p_{n}(x_{n})}'s restriction to C is a sequence {\displaystyle a_{1},a_{2},\ldots ,a_{n}} such that

And so on, down to

In the example of ACF, associativity means that the generic type of {\displaystyle (V_{1}\times V_{2})\times V_{3}} is the same as the generic type of {\displaystyle V_{1}\times (V_{2}\times V_{3})}, which is clear.

[]{#.28Failure_of.29_Commutativity}[(Failure of) Commutativity]{#(Failure_of)_Commutativity .mw-headline}[]

Two global invariant types p(x) and q(y) are said to commute if {\displaystyle p(x)\otimes q(y)=q(y)\otimes p(x)}. In other words,

{\displaystyle (a,b)\models p\otimes q\upharpoonright C\iff (b,a)\models q\otimes p\upharpoonright C}.

(This is not the same as saying that {\displaystyle p\otimes q} is {\displaystyle q\otimes p}; the variables must be kept track of.)

Ideally, commutativity would always happen. This is the case in stable theories, and in NIP theories when one of the types is generically stable. In the example of ACF, this reflects the fact that if {\displaystyle (a,b)} is a generic point on {\displaystyle V\times W}, then {\displaystyle (b,a)} is a generic point on {\displaystyle W\times V}.

Here is an example of failure of commutativity. In the theory of dense linear orders, let p be the definable 1-type at +∞. This is Ø-invariant. If C is a small subset of the monster, then {\displaystyle (a,b)\models p(x)\otimes p(y)\upharpoonright C} if b > C (i.e., b is bigger than every element of C) and a > b. But of course this is different from {\displaystyle (b,a)\models p(x)}, which implies that b > a > C. So p does not even commute with itself.

Morley Sequences of Invariant Types[]

If p is a global A-invariant type, a Morley sequence in the type p is a sequence {\displaystyle a_{1},a_{2},\ldots } where

{\displaystyle a_{i}\models p\upharpoonright Aa_{1}a_{2}\cdots a_{i-1}}

for each i. This definition easily generalizes to Morley sequences of any ordinal length.

Theorem: A Morley sequence in the type p is indiscernible over A'. Any two Morley sequences in p have the same type over A (assuming they have the same length).

Proof: Let {\displaystyle a_{1},a_{2},\ldots } be a Morley sequence. Note that if {\displaystyle i_{1}<\cdots <i_{n}} then for 1 ≤ kn, {\displaystyle a_{i_{k}}} realizes {\displaystyle p\upharpoonright Aa_{i_{1}}\cdots a_{i_{k-1}}}, because {\displaystyle \{a_{i_{1}},\ldots ,a_{i_{k-1}}\}\subseteq \{a_{1},\ldots ,a_{i_{k}}\}}. It follows that

{\displaystyle (a_{i_{k}},a_{i_{k-1}},\ldots ,a_{i_{1}})\models p(x_{1})\otimes \cdots \otimes p(x_{n})\upharpoonright A}

Consequently, if {\displaystyle j_{1}<\cdots j_{n}} is some other ascending sequence, then

{\displaystyle (a_{i_{k}},a_{i_{k-1}},\ldots ,a_{i_{1}})} and {\displaystyle (a_{j_{k}},a_{j_{k-1}},\ldots ,a_{j_{1}})} both realize {\displaystyle p^{\otimes n}\upharpoonright A}.

Therefore, we have indiscernibility. Also, if {\displaystyle b_{1},b_{2},\ldots } is some other Morley sequence, then for each n,

{\displaystyle (a_{n},a_{n-1},\ldots ,a_{1})} and {\displaystyle (b_{n},b_{n-1},\ldots ,b_{1})} both realize {\displaystyle p^{\otimes n}\upharpoonright A}.

So {\displaystyle a_{1}\cdots a_{n}\equiv _{A}b_{1}\cdots b_{n}}. Since this happens for all n, the two Morley sequences have the same type over A. (This argument can easily be modified to handle the case of Morley sequences of length more than {\displaystyle \omega }.)

QED.

Morley sequences of this type play a key role in elementary stability theory, where they can be used to prove the definability of types in stable theories.

Also, we can use this kind of Morley sequence to prove the existence of non-trivial indiscernible sequences.

Corollary: Let M be a structure with an infinite total ordering < (one one of the sorts). Then there is an elementary extension of M in which there is a strictly increasing indiscernible sequence {\displaystyle a_{1}<a_{2}<\cdots }.

Proof: Let {\displaystyle {\mathfrak {M}}} be a monster model of the complete theory of M. Since M (or its totally ordered sort) is infinite, there is some complete type p over M which lives in the ordered sort, but is not realized in M (i.e., is not constant). Let q be a global M-invariant extension of p, which exists for reasons explained above. If q were realized in {\displaystyle {\mathfrak {M}}} then q(x) would be a constant type of the form x = a for some a from {\displaystyle {\mathfrak {M}}}. Then by M-invariance, a would need to be fixed by every automorphism which fixes M. This would force a to be in the definable closure of M, which is M. So q(x) includes the statement x = a, and so does p(x), contradicting the assumption that p is not a constant type.

So q is not a constant type. Then for any small set C and any cC, the formula xc is in {\displaystyle q(x)\upharpoonright C}.

In particular, if {\displaystyle a_{1},a_{2},\ldots } is a Morley sequence for q, then {\displaystyle a_{i}\models q\upharpoonright Ma_{1}\ldots a_{i-1}}, so {\displaystyle a_{i}\notin \{a_{1},\ldots ,a_{i-1}\}}. In other words, no two elements of the Morley sequence are equal. Also, the sequence is M-indiscernible, hence indiscernible (over the empty set).

Because the ordering is total, either {\displaystyle a_{1}<a_{2}} or {\displaystyle a_{1}>a_{2}}. In the former case, indiscernibility implies that {\displaystyle a_{i}<a_{i+1}} for every i, so the sequence is increasing and we are done. Otherwise, we can extract an indiscernible sequence of the same Ehrenfeucht-Mostowski type, but indexed by the negative integers

{\displaystyle \ldots ,b_{-3},b_{-2},b_{-1}}.

As part of the EM type, we see that

{\displaystyle \cdots >b_{-3}>b_{-2}>b_{-1}}

Then

{\displaystyle b_{-1}<b_{-2}<b_{-3}<\cdots }

is our desired increasing indiscernible sequence.

In more detail (without mentioning EM types), consider the infinitary partial type {\displaystyle \Sigma (x_{1},x_{2},x_{3},\ldots )} consisting of the statements asserting indiscernibility of {\displaystyle (x_{1},x_{2},\ldots )} together with {\displaystyle x_{1}<x_{2}}. Then {\displaystyle \Sigma (x_{1},x_{2},\ldots )} is consistent, because if {\displaystyle \Sigma _{0}(x_{1},x_{2},\ldots )} is a finite subset, then {\displaystyle \Sigma _{0}} only mentions {\displaystyle x_{1},\ldots ,x_{n}} for some n, and then

{\displaystyle (a_{n},a_{n-1},\ldots ,a_{1},garbage)\models \Sigma _{0}(x_{1},\ldots ,x_{n},\ldots )}

Any realization of the consistent type {\displaystyle \Sigma (x_{1},x_{2},\ldots )} will yield our desired indiscernible sequence.

Having found the increasing indiscernible sequence, we can pass to a small model if we like, or just stick with the monster {\displaystyle {\mathfrak {M}}} as our elementary extension of M.

QED.

From this, it is not hard to prove that indiscernible sequences can be extracted in general.

Corollary: Let M be a structure, and let {\displaystyle \{a_{i}\}_{i\in I}} be any infinite sequence (with I an ordered set). Then we can find an elementary extension of M in which there is an indiscernible sequence realizing the EM type of {\displaystyle \{a_{i}\}_{i\in I}}.

Proof: Consider the auxiliary structure {\displaystyle M'} obtained by adding I as a new sort, and adding symbols for the total ordering on I and a function symbol f for the map {\displaystyle i\mapsto a_{i}}. By the previous Corollary, we can find an elementary extension {\displaystyle N'\succeq M'} containing an increasing indiscernible sequence {\displaystyle \alpha _{1}<\alpha _{2}<\cdots } in the new I sort. Then {\displaystyle f(\alpha _{1}),f(\alpha _{2}),\ldots } is certainly indiscernible in {\displaystyle N'}. Let N be the reduct of {\displaystyle N'} to the original language (dropping the extra I sort). Then N is an elementary extension of M. Also, {\displaystyle f(\alpha _{1}),f(\alpha _{2}),\ldots } is certainly indiscernible in N.

Finally, we check that this indiscernible sequence satisfies the correct EM type. Suppose that {\displaystyle \phi (x_{1},\ldots ,x_{n})} is a formula in the EM type of {\displaystyle \{a_{i}\}_{i\in I}}. This means that

{\displaystyle M\models \phi (a_{i_{1}},\ldots ,a_{i_{n}})} whenever {\displaystyle i_{1}<\ldots i_{n}}.

But then

{\displaystyle M'\models \forall x_{1},\ldots x_{n}:x_{1}<x_{2}<\cdots x_{n}\rightarrow \phi (f(x_{1}),\ldots ,f(x_{n}))}.

Of course the same thing must hold in {\displaystyle N'}, which means that for any {\displaystyle j_{1}<j_{2}<\ldots <j_{n}},

{\displaystyle N'\models \phi (f(\alpha _{j_{1}}),f(\alpha _{j_{2}}),\ldots ,f(\alpha _{j_{n}})},

because {\displaystyle \alpha _{j_{1}}<\cdots <\alpha _{j_{n}}}.

Then since {\displaystyle \phi } was a formula in the original language,

{\displaystyle N\models \phi (f(\alpha _{j_{1}}),\ldots ,f(\alpha _{j_{n}}))}.

As this holds for any {\displaystyle j_{1}<j_{2}<\cdots <j_{n}}, the sequence {\displaystyle f(\alpha _{1}),f(\alpha _{2}),\ldots } really does satisfy the correct EM type.

QED. ::: ::: :::