# Today I Learned

Some of the things I've learned every day since Oct 10, 2016

## 187: Craig Interpolation Theorem

Where $\Gamma$ is a set of first-order formulas, let $\mathcal{A}_\Gamma$ be the set of function, relation, and constant symbols which occur in $\Gamma$. That is, the smallest set $\mathcal{A}$ such that each formula of $\Gamma$ is an $\mathcal{L}_{\mathcal{A}}$-formula.

Suppose that $\Gamma$ is any set of formulas, $\varphi_1, \varphi_2$ are formulas, $\Gamma \vdash (\varphi_1 \rightarrow \varphi_2)$, and that $\mathcal{A}_{\{\varphi_1\}} \cap \mathcal{A}_{\{\varphi_2\}} \subseteq \mathcal{A}_\Gamma$. Then the Craig Interpolation Theorem states that there is an $\mathcal{L}_{\mathcal{A}_\Gamma}$-formula $\psi$, the interpolant, such that

$\Gamma \vdash (\varphi_1 \rightarrow \psi)$

and

$\Gamma \vdash (\psi \rightarrow \varphi_2)$.