Definable types over stably embedded sets Let $T$ be a complete $\mathcal{L}$-theory and $\mathfrak{U}$ a monster model, with $\theta(v)$ an $\mathcal{L}$-formula and $M\preccurlyeq \mathfrak{U}$ a (not necessarily small) model. We say that $\theta(M)$ is stably embedded in $M$ if, for every $\mathcal{L}_M$-formula $\varphi(v_1,\dots,v_n,\overline{m})$, the formula $\varphi(v_1,\dots,v_n,\overline{m})\wedge\bigwedge_{i=1}^n\theta(v_i)$ is equivalent to some $\mathcal{L}_{\theta(M)}$ formula. The following exercise is from Tent and Ziegler:

Exercise 8.3.4: Show that $\theta(M)$ is stably embedded in $M$ if and only if, for all $n$, every $p\in S_n(\theta(M))$ which contains $\bigwedge_{i=1}^n\theta(v_i)$ has a unique extension $\overline{p}\in S_n(M)$. If $\theta$ is absolutely stably embedded and $p$ is definable, show that $\overline{p}$ is definable over $\theta(M)$.

I've done the first part of the problem, for which one direction is clear; indeed, if $p_1,p_2\in S_n(M)$ are distinct extensions of $p$, let $\varphi(\overline{v},\overline{m})$ be a separating formula, with $\varphi\in p_1$ and $\neg\varphi\in p_2$. Since $\bigwedge_{i=1}^n\theta(v_i)\in p_1,p_2$, letting $\varphi'=\varphi(\overline{v},\overline{m})\wedge\bigwedge_{i=1}^n\theta(v_i)$ still gives $\varphi'\in p_1$ and $\neg\varphi'\in p_2$. If $\theta(M)$ were stably embedded, then $\varphi'$ would be equivalent to an $\mathcal{L}_{\theta(M)}$-formula, and then either that formula or its negation would lie in $p$, which would make one of $p_1$ or $p_2$ inconsistent.
The other direction seems to require a bit more work; suppose any type in $S_n(\theta(M))$ containing $\bigwedge_{i=1}^n\theta(v_i)$ has a unique extension to $S_n(M)$, and let $\varphi(v_1,\dots,v_n,\overline{m})$ be any $\mathcal{L}_M$-formula such that $\varphi\to\bigwedge_{i=1}^n\theta(v_i)$. We wish to show that $\varphi$ is equivalent to some $\mathcal{L}_{\theta(M)}$ formula. To see this, enumerate the stone space $S_n(\theta(M))$ as $(p_\alpha)_{\alpha\in\lambda}$ for some cardinal $\lambda$, and define
\begin{align}
A&=\{\alpha\in\lambda:p_\alpha\cup\{\varphi(\overline{v},\overline{m})\}\text{ is consistent}\} \\
B&=\{\beta\in\lambda:p_\beta\cup\{\neg\varphi(\overline{v},\overline{m})\}\text{ is consistent}\}.
\end{align}
We claim $S_n(\theta(M))=A\sqcup B$. That $S_n(\theta(M))=A\cup B$ is clear, and disjointness follows from the hypothesis on types. Indeed, if $p_\alpha$ is consistent with $\varphi(\overline{v},\overline{m})$, then it must contain $\bigwedge_{i=1}^n\theta(v_i)$, and so by the hypothesis has a unique extension to $S_n(M)$. This extension must contain $\varphi(\overline{v},\overline{m})$, and so $p_\alpha$ is inconsistent with $\neg\varphi(\overline{v},\overline{m})$, whence $\alpha\notin B$, as desired. Thus, for any $\alpha\in A$ and $\beta\in B$, we can choose $\psi_{\alpha\beta}$ with $\psi_{\alpha\beta}\in p_\alpha$ and $\neg\psi_{\alpha\beta}\in p_\beta$; note in particular that $\psi_{\alpha\beta}$ is an $\mathcal{L}_{\theta(M)}$-formula.
Now, fix $\alpha\in A$. Since any type over $M$ containing $\neg\varphi$ must contain $p_\beta$ for some $\beta\in B$, we have $\{\psi_{\alpha\beta}\}_{\beta\in B}\models \varphi$, and thus there are $\beta_1,\dots,\beta_k$ such that $\{\psi_{\alpha\beta_i}\}_{i=1}^k\models\varphi$. Let $\eta_\alpha=\bigwedge_{i=1}^k\psi_{\alpha\beta_i}$, so that $\eta_\alpha\to\varphi$ and $\eta_\alpha\in p_\alpha$. Since every type over $M$ containing $\varphi$ must be $p_\alpha$ for some $\alpha\in A$, this latter condition means $\{\neg\eta_\alpha\}_{\alpha\in A}\models \neg\varphi$, and thus there are $\alpha_1,\dots,\alpha_k$ with $\{\neg\eta_{\alpha_i}\}_{i=1}^k\models\neg\varphi$. Then, letting $\eta=\bigvee_{i=1}^k\eta_{\alpha_i}$, we have $\varphi\leftrightarrow\eta$, and by construction $\eta$ is an $\mathcal{L}_{\theta(M)}$-formula, as desired.
So this wraps up the first part. Unfortunately, I'm struggling a bit with the second part. For one thing, I'm not actually sure what T&Z mean by "absolutely" stably embedded; this isn't a term they've defined. I assume this result doesn't hold in the general case, or else they wouldn't add that qualifier, but for now I've only been trying to approach it in general. Perhaps it will be clearer once I know the right hypotheses?
Anyway, let $\varphi(\overline{v},\overline{w})$ be an $\mathcal{L}$-formula; we may assume $\varphi(\overline{v},\overline{w})\to\bigwedge_{i=1}^n\theta(v_i)$. For any $\overline{m}\in M$, we then know that $\varphi(\overline{v},\overline{m})$ is equivalent to some $\theta(M)$-formula $\psi_\overline{m}(\overline{v},\overline{a}_\overline{m})$, and so $\varphi(\overline{v},\overline{m})\in\overline{p}$ if and only if $\psi_\overline{m}(\overline{v},\overline{a}_\overline{m})\in p$. Thus, if there were some way to choose all the $\psi_\overline{m}(\overline{v},\overline{u})$ to be equal, we would be done, since we would have $$\varphi(\overline{v},\overline{m})\in \overline{p}\iff\mathfrak{U}\models\exists \overline{u}\left[\bigwedge_{i=1}^k \theta(u_i)\wedge\left[\forall\overline{v}\varphi(\overline{v},\overline{m})\leftrightarrow\psi(\overline{v},\overline{u})\right]\wedge d_p\overline{v}\psi(\overline{v},\overline{u})\right],$$ where $\psi=\psi_\overline{m}$ for all $\overline{m}$ and $d_p\overline{v}$ denotes the definition of $p$ over $\theta(M)$. However, I'm not so sure how we might go about removing the dependence on $\overline{m}$, and presumably we can't in general; does the "absolute" hypothesis somehow make this possible? Is this even a good approach, or does it not work?
 A: You've correctly identified the sticking point in your suggested proof: Every formula $\varphi(v,m)$ with $m\in M$ is equivalent to some formula $\psi_m(v,n)$ with $n\in \theta(M)$, but which formula $\psi_m$ works apparently depends on $\varphi$ and $m$, and we would like it to depend just on $\varphi$.
One of the most important tricks in the model theory toolbox is using the compactness theorem to get "uniformity for free". We often know something of the form "In every model $M$, for every definable set $X$, there exists a definable set $Y$ such that..." Then we can use the compactness theorem to show that when we restrict to those $X$ which are defined by instances of a formula $\varphi$, there must be finitely many formulas $\psi_1,\dots,\psi_k$ such that the witnessing $Y$ is defined by an instance of one of the $\psi_i$. And finally, we can code the finitely many $\psi_i$ into a single formula and conclude "For every formula $\varphi$ there is a formula $\psi$ such that for every instance $X$ of $\varphi$ there is an instance $Y$ of $\psi$ such that..."
At this point, you might like to use the above as a hint and try to solve the exercise yourself. But if you get stuck, here are the details.
Suppose $\theta(M)$ is stably embedded in $M$ for every $M\models T$. To simplify notation, I'll write all tuples of variables as if they were singletons. Fix a formula $\varphi(v,w)$ which implies $\theta(v)$. Consider the following partial type in the variables $w$: $$T\cup \{\lnot \exists z\,(\theta(z)\land \forall v\, (\varphi(v,w)\leftrightarrow \psi(v,z)))\mid \psi(v,z)\in \mathcal{L}\}.$$
This partial type is inconsistent (this is where we need to use stable embeddedness in every small model, or equivalently in the monster model). So by compactness there are finitely many formulas $\psi_1(v,z_1),\dots,\psi_k(v,z_k)\in \mathcal{L}$ such that $$T\models \forall w\, \bigvee_{i=1}^k \exists z_i\,(\theta(z_i)\land \forall v\, (\varphi(v,w)\leftrightarrow \psi_i(v,z_i))).$$
Now by the standard trick of coding finitely many formulas by a single formula (which I described, for example, here), we may assume there is a single formula $\psi(v,z)$ such that for every model $M$ and every instance of $\varphi(v,w)$ with parameters from $M$, there is an equivalent instance of $\psi(v,z)$ with parameters from $\theta(M)$.
[Technical note: To do this coding, we need to assume that $\theta(M)$ has as least two elements. But if $\theta(M)$ has at most one element, then any complete type which implies $\theta(v)$ is realized in $M$, and hence definable.]
Finally, we can conclude as you did, writing down an explicit definition over $\theta(M)$ for any type containing $\theta(v)$ which is definable over $M$.
