Morley sequences of arbitrary order type

Question

A sequence $(a_j \,|\, j \in J)$ is called independent over $A$ if $a_j \underset{A}{\overset{\vert}{\smile}} \left\{a_k \,|\, k < j \right\}$ for every $j$, i.$\,$e. $\text{tp}(a_j/A \cup \left\{a_k \,|\, k < j \right\})$ does not fork over $A$. A sequence is called a Morley sequence over $A$ if it is both independent and indiscernible over $A$.

I would like to prove the following: For every Morley sequence $(a_j \,|\, j \in J)$ and every infinite linear order $I$ there is a Morley sequence $(b_i \,|\, i \in I)$ which satisfies the Ehrenfeucht-Mostowski type $\mathcal{E\!M}((a_j)_{j \in J} /A)$ of $(a_j)_{j \in J}$ over $A$.

By the standard lemma it follows that there is an indiscernible sequence $(b_i \,|\, i \in I)$ satisying $\mathcal{E\!M}((a_j)_{j \in J} /A)$. However I do not see why it should be independent.

It seems that the statement is used in Tent and Ziegler's book (proof of proposition 7.2.14).

Answer 1

It's because forking is always witnessed by a formula ("finite character"), and whether a formula $\varphi(x,c)$ forks over $A$ just depends on $\text{tp}(c/A)$ ("invariance").

Suppose that $(b_i)_{i\in I}$ is not independent. Then there is some $k\in I$ such that $\text{tp}(b_k/Ab_{<k})$ forks over $A$ (notation: $b_{<k} = \{b_i\mid i<k\}$). This is witnessed by some formula $\varphi(x,b_{i_1},\dots,b_{i_n},c)\in \text{tp}(b_k/Ab_{<k})$ which forks over $A$, where $c$ is a tuple from $A$ and $i_1<\dots<i_n<k\in I$.

Now since $(b_i)_{i\in I}$ satisfies $\mathcal{EM}((a_j)_{j\in J}/A)$, pick any $j_1<\dots<j_n<k'\in J$, and we have:

1. $\varphi(x,a_{j_1},\dots,a_{j_n},c)$ forks over $A$ (since $\text{tp}(a_{j_1} \dots a_{j_n}c/A) = \text{tp}(b_{i_1}\dots b_{i_n}c/A)$), and
2. $\varphi(x,a_{j_1},\dots,a_{j_n},c)\in \text{tp}(a_{k'}/Aa_{<k'})$ (since $\text{tp}(a_{j_1}\dots a_{j_n}a_{k'}c/A) = \text{tp}(b_{i_1}\dots b_{i_n}b_kc/A)$).

So $\text{tp}(a_{k'}/Aa_{<k'})$ forks over $A$, contradicting our assumption that $(a_j)_{j\in J}$ is a Morley sequence.