[proofplan]
We compare two descriptions of isolation. The definition says that an isolating formula $\theta(x)$ belongs to the type and forces every formula of the type over the base theory with parameters. Completeness of the type supplies the converse test: if a formula is not in $p(x)$, then its negation is in $p(x)$, so $\theta(x)$ cannot also force the formula without making the type inconsistent. The reverse implication is then immediate because the displayed equivalence says precisely that every member of $p(x)$ is entailed by $\theta(x)$ over $T_A$.
[/proofplan]
[step:Fix the base theory with parameters and recall consistency for the type]
Define
\begin{align*}
T_A := T \cup \operatorname{Diag}(A).
\end{align*}
Since $p(x)$ is a complete $n$-type over $A$, it is a maximal $T_A$-consistent set of $L(A)$-formulas in the free variables $x = (x_1,\dots,x_n)$. In particular, for every $L(A)$-formula $\varphi(x)$, exactly one of $\varphi(x)$ and $\neg \varphi(x)$ belongs to $p(x)$.
We use the standard definition that an $L(A)$-formula $\theta(x)$ isolates $p(x)$ when $\theta(x) \in p(x)$ and, for every $L(A)$-formula $\psi(x) \in p(x)$,
\begin{align*}
T_A \models \forall x\,(\theta(x) \to \psi(x)).
\end{align*}
[/step]
[step:Show that an isolating formula entails exactly the formulas in the type]
Assume that $\theta(x)$ isolates $p(x)$. Then $\theta(x) \in p(x)$ by definition. Let $\varphi(x)$ be an arbitrary $L(A)$-formula.
First suppose $\varphi(x) \in p(x)$. Since $\theta(x)$ isolates $p(x)$, the defining property of isolation gives
\begin{align*}
T_A \models \forall x\,(\theta(x) \to \varphi(x)).
\end{align*}
Conversely, suppose
\begin{align*}
T_A \models \forall x\,(\theta(x) \to \varphi(x)).
\end{align*}
If $\varphi(x) \notin p(x)$, then completeness of $p(x)$ gives $\neg \varphi(x) \in p(x)$. Because $\theta(x) \in p(x)$ as well, the finite subset $\{\theta(x),\neg\varphi(x)\}$ of $p(x)$ must be $T_A$-consistent. But the displayed entailment says that
\begin{align*}
T_A \models \forall x\,(\theta(x) \to \varphi(x)),
\end{align*}
so $T_A \cup \{\theta(x),\neg\varphi(x)\}$ is inconsistent. This contradicts the $T_A$-consistency of $p(x)$. Therefore $\varphi(x) \in p(x)$.
Since $\varphi(x)$ was arbitrary, for every $L(A)$-formula $\varphi(x)$,
\begin{align*}
\varphi(x) \in p(x)
\quad \Longleftrightarrow \quad
T_A \models \forall x\,(\theta(x) \to \varphi(x)).
\end{align*}
[guided]
Assume that $\theta(x)$ isolates $p(x)$. The definition of isolation has two parts: first, $\theta(x)$ itself lies in the type, so $\theta(x) \in p(x)$; second, every formula already in the type is forced by $\theta(x)$ over the parameter theory $T_A$.
Let $\varphi(x)$ be an arbitrary $L(A)$-formula. We must prove both directions of the equivalence.
If $\varphi(x) \in p(x)$, then the isolating property applies directly to $\varphi(x)$. Hence
\begin{align*}
T_A \models \forall x\,(\theta(x) \to \varphi(x)).
\end{align*}
For the converse, suppose
\begin{align*}
T_A \models \forall x\,(\theta(x) \to \varphi(x)).
\end{align*}
We want to prove that $\varphi(x) \in p(x)$. Since $p(x)$ is complete, there are only two possibilities: either $\varphi(x) \in p(x)$ or $\neg\varphi(x) \in p(x)$. Assume for contradiction that $\varphi(x) \notin p(x)$. Then completeness gives
\begin{align*}
\neg\varphi(x) \in p(x).
\end{align*}
Also $\theta(x) \in p(x)$ because $\theta(x)$ isolates $p(x)$. Since a type is $T_A$-consistent, every finite subset of it is satisfiable with $T_A$; in particular,
\begin{align*}
T_A \cup \{\theta(x),\neg\varphi(x)\}
\end{align*}
must be consistent. But the semantic entailment
\begin{align*}
T_A \models \forall x\,(\theta(x) \to \varphi(x))
\end{align*}
says that no realization of $\theta(x)$ in any model of $T_A$ can satisfy $\neg\varphi(x)$. Thus
\begin{align*}
T_A \cup \{\theta(x),\neg\varphi(x)\}
\end{align*}
is inconsistent, a contradiction. Therefore the alternative $\neg\varphi(x) \in p(x)$ is impossible, and so $\varphi(x) \in p(x)$.
This proves that $\theta(x)$ entails exactly the formulas belonging to $p(x)$.
[/guided]
[/step]
[step:Recover isolation from the displayed equivalence]
Assume that $\theta(x) \in p(x)$ and that for every $L(A)$-formula $\varphi(x)$,
\begin{align*}
\varphi(x) \in p(x)
\quad \Longleftrightarrow \quad
T_A \models \forall x\,(\theta(x) \to \varphi(x)).
\end{align*}
Let $\psi(x) \in p(x)$ be arbitrary. Applying the displayed equivalence with $\varphi(x) := \psi(x)$ gives
\begin{align*}
T_A \models \forall x\,(\theta(x) \to \psi(x)).
\end{align*}
Thus $\theta(x) \in p(x)$ and $\theta(x)$ entails every formula of $p(x)$ over $T_A$. By the definition of isolation, $\theta(x)$ isolates $p(x)$.
[/step]
[step:Identify the equivalent decision formulation]
The displayed equivalence implies the decision formulation. Let $\varphi(x)$ be an arbitrary $L(A)$-formula. Since $p(x)$ is complete, exactly one of $\varphi(x)$ and $\neg\varphi(x)$ belongs to $p(x)$. If $\varphi(x) \in p(x)$, then
\begin{align*}
T_A \models \forall x\,(\theta(x) \to \varphi(x)).
\end{align*}
If $\neg\varphi(x) \in p(x)$, then applying the displayed equivalence to $\neg\varphi(x)$ gives
\begin{align*}
T_A \models \forall x\,(\theta(x) \to \neg\varphi(x)).
\end{align*}
Thus $\theta(x)$ decides every $L(A)$-formula over $T_A$, and the decision agrees with membership in $p(x)$.
Conversely, if $\theta(x) \in p(x)$ and $\theta(x)$ decides every $L(A)$-formula over $T_A$ with the decision agreeing with $p(x)$, then for each $L(A)$-formula $\varphi(x)$,
\begin{align*}
\varphi(x) \in p(x)
\quad \Longleftrightarrow \quad
T_A \models \forall x\,(\theta(x) \to \varphi(x)).
\end{align*}
Therefore the decision formulation is equivalent to the displayed criterion, and the theorem follows.
[/step]
