Proof of Lyndon's interpolation theorem

Proof

We present here a constructive proof of the Craig interpolation theorem for propositional logic.

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.

Craig interpolation can be proved by other methods as well. However, these proofs are generally non-constructive:

• model-theoretically, via Robinson's joint consistency theorem: in the presence of compactness, negation and conjunction, Robinson's joint consistency theorem and Craig interpolation are equivalent.
• proof-theoretically, via a sequent calculus. If cut elimination is possible and as a result the subformula property holds, then Craig interpolation is provable via induction over the derivations.
• algebraically, using amalgamation theorems for the variety of algebras representing the logic.
• via translation to other logics enjoying Craig interpolation.