Craig interpolation theorem

Remarks

The sentence $\theta$ is called an interpolant. One proof uses a cut-free sequent calculus and builds $\theta$ by induction on a cut-free proof of $\varphi \to \psi$. Another proof is model-theoretic and uses the compactness theorem. Example: $P(c) \land Q(c) \models P(c) \lor R(c)$, and $\theta = P(c)$ is an interpolant in the common symbols $P$ and $c$. When $\varphi$ and $\psi$ share no symbols, $\theta$ is a sentence of pure equality, such as $\forall x \, (x = x)$ or its negation. The propositional version holds too, with $\theta$ built from the common variables and the constants $\top$ and $\bot$. William Craig proved the theorem in 1957.

Going deeper

For a student

Craig interpolation is a basic structural property of first-order logic. It implies the Beth definability theorem: an implicitly definable relation is explicitly definable. It is closely related to Robinson's joint consistency theorem. Many other logics fail to have it, so it is also used to compare logics.