\begin{definition}[Definition:Isolated Type]
Let $T$ be an $\LL$-theory.
Let $\map \phi {\bar v}$ be an $\LL$-formula in $n$ free variables $\bar v$ such that $T \cup \map \phi {\bar v}$ is satisfiable.
{{Disambiguate|Definition:Logical Formula}}
Let $p$ be an $n$-type of $T$.
We say that $\phi$ '''isolates''' $p$ {{iff}} for all $\psi \in p$, we have:
:$T \models \forall \map {\bar v} {\map \phi {\bar v} \rightarrow \map \psi {\bar v} }$
that is, all $\psi$ are semantic consequences of $\phi$.
Category:Definitions/Model Theory
\end{definition}