= Propositional interpolation
{title2=$A\vdash C\vdash B$}
If $A\vdash B$, eliminate the letters private to $A$ by
$$
C=\bigvee_{\varepsilon:\operatorname{Var}(A)\setminus\operatorname{Var}(B)\to\{0,1\}}A[\varepsilon].
$$
Every assignment satisfying $A$ satisfies one disjunct of $C$. If an assignment satisfies $C$, change only the eliminated letters to its witnessing assignment. The modified assignment satisfies $A$ and hence $B$, whose letters were unchanged. Thus $A\models C\models B$, and the <propositional completeness theorem> gives the two derivations. The interpolant uses only common letters; an empty common vocabulary is handled by logical truth constants.
Back to article page
