Roughly stated, the theorem says that if a formula φ implies a formula ψ, and the two have at least one atomic variable symbol in common, then there is a formula ρ, called an interpolant, such that every non-logical symbol in ρ occurs both in φ and ψ, φ implies ρ, and ρ implies ψ.
The theorem was first proved for first-order logic by William Craig in 1957.
A stronger form of Craig's interpolation theorem for first-order logic was proved by Roger Lyndon in 1959;[1][2] the overall result is sometimes called the Craig–Lyndon theorem.
Lyndon's theorem says that if S ∪ T is unsatisfiable, then there is an interpolating sentence ρ in the language of S ∩ T that is true in all models of S and false in all models of T. Moreover, ρ has the stronger property that every relation symbol that has a positive occurrence in ρ has a positive occurrence in some formula of S and a negative occurrence in some formula of T, and every relation symbol with a negative occurrence in ρ has a negative occurrence in some formula of S and a positive occurrence in some formula of T. We present here a constructive proof of the Craig interpolation theorem for propositional logic.
Here atoms(φ) is the set of propositional variables occurring in φ, and ⊨ is the semantic entailment relation for propositional logic.
The proof proceeds by induction on the number of propositional variables occurring in φ that do not occur in ψ, denoted |atoms(φ) − atoms(ψ)|.
This suffices to show that φ is a suitable interpolant in this case.
Let’s assume for the inductive step that the result has been shown for all χ where |atoms(χ) − atoms(ψ)| = n. Now assume that |atoms(φ) − atoms(ψ)| = n+1.
We may observe three things from this definition: From (1), (2) and the inductive step we have that there is an interpolant ρ such that: But from (3) and (4) we know that Hence, ρ is a suitable interpolant for φ and ψ.
Since the above proof is constructive, one may extract an algorithm for computing interpolants.
Using this algorithm, if n = |atoms(φ') − atoms(ψ)|, then the interpolant ρ has O(exp(n)) more logical connectives than φ (see Big O Notation for details regarding this assertion).
Similar constructive proofs may be provided for the basic modal logic K, intuitionistic logic and μ-calculus, with similar complexity measures.