A theorem to the effect that if $\phi \models \psi$ (for some notion of logical consequence $\models$), and $\phi$ and $\psi$ have some non-logical vocabulary in common, then there is a formula $\xi$, all the non-logical symbols of which occur in both $\phi$ and $\psi$, such that $\phi \models \xi$ and $\xi \models \psi$. $\xi$ is called the interpolant.