A type over a model does not fork over the model I have been trying to show that a complete type $p$ over a model $M$ does not fork over the model $M$.
I have been trying to show this as follows: suppose that $\chi(x, m) \in p$ has that $\models \chi(x, m) \rightarrow \phi(x, a) \vee \psi(x, b)$ where $\phi(x, a)$ and $\psi(x, b)$ divide over $M$ (there can be more dividing formulas, but I'm trying to keep the notation simple.)  Since $M$ is the elementary submodel of the monster, we have $\models \chi(x, m) \rightarrow \phi(x, a') \lor \psi(x, b')$ for some $a'b' \in M$.  Since $p$ is complete, it has either $\phi(x, a')$ or $\psi(x, b')$.  Say it's $\phi(x, a')$.  Now I want an $M$-indiscernible sequence starting at $a'$ witnessing the dividing of $\phi(x, a')$ (to derive a contradiction - nothing divides over its own parameter set).
I thought I could do this from the indiscernible sequence witnessing the dividing of $\phi(x, a)$, but I fail to see how.  Am I misguided? 
 A: Rather than moving the parameters in the dividing formulas $\phi$ and $\psi$ into $M$, you want to move an element realizing the forking formula $\chi$ into $M$.
Here's a proof: Suppose $p\in S(M)$ and $\chi(x,m)\in p$ such that $\chi(x,m)\rightarrow \bigvee_{i=1}^k \phi_i(x,a_i)$ and each $\phi_i(x,a_i)$ divides over $M$. Since $\chi(x,m)$ is consistent, we can find $b\in M$ such that $M\models \chi(b,m)$. Then for some $1\leq i\leq k$, we have $\models \phi_i(b,a_i)$. Pick a sequence $(c_j)_{j\in \omega}$ with $c_0 = a_i$ witnessing the dividing of $\phi_i(x,a_i)$. But since $c_j$ satisfies $\mathrm{tp}(a_i/M)$ for all $i$, and $b\in M$, we have $\models \phi_i(b,c_j)$ for all $j$, contradicting the definition of dividing.
Here's an exercise: Generalize this to show that if $p\in S(B)$ is finitely satisfiable in $A\subseteq B$ (meaning that for all $\psi(x,b)\in p$, there exists $a\in A$ such that $\models \psi(a,b)$; we also say that $p$ is a coheir of its restriction to $A$), then $p$ does not fork over $A$. Then the observation about models is just that every type over a model $M$ is finitely satisfiable in $M$.
Here's some more discussion: The dual notion to coheir is heir. $p\in S(B)$ is an heir of its restriction to $A$ if for every formula $\psi(x,b)\in p$, there exists $a\in A$ such that $\psi(x,a)\in p$. In a stable theory, when $M$ is a model and $M\subseteq B$, $p\in S(B)$ is an heir of its restriction to $M$ if and only if $p$ is a coheir of its restriction to $M$ if and only if $p$ does not fork over $M$. 
But in a general theory, even over models, heirs and coheirs can be different, there can be nonforking extensions which are not coheirs, and there can be heirs which are not nonforking extensions. For example, let $M\models \mathrm{DLO}$, and let $A = M\cup \{a\}$, where $a$ is greater than all the elements of $M$. Then:


*

*The complete type in $S(A)$ isolated by $x>a$ is an heir of its restriction to $M$ but is not a coheir. It does not fork over $M$.

*The complete type in $S(A)$ determined by $\{x>m\mid m\in M\}\cup \{x<a\}$ is a coheir of its restriction to $M$ but is not an heir. It also does not fork over $M$.

*Let $b$ and $c$ be two elements living in some cut in $M$, so $b<c$ and for every $m\in M$, either $m< b$ or $c < m$. Let $B = M\cup \{b,c\}$. The complete type in $S(B)$ isolated by $b<x \land x < c$ is an heir of its restriction to $M$, and it forks over $M$.

