Craig interpolation

Lyndon's interpolation theorem

Suppose that S and T are two first-order theories. As notation, let S ∪ T denote the smallest theory including both S and T; the signature of S ∪ T is the smallest one containing the signatures of S and T. Also let S ∩ T be the intersection of the languages of the two theories; the signature of S ∩ T is the intersection of the signatures of the two languages.

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.

Proof of Craig's interpolation theorem

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

Theorem— If ⊨φ → ψ then there is a ρ (the interpolant) such that ⊨φ → ρ and ⊨ρ → ψ, where atoms(ρ) ⊆ atoms(φ) ∩ atoms(ψ). Here atoms(φ) is the set of propositional variables occurring in φ, and ⊨ is the semantic entailment relation for propositional logic.

Proof

Assume ⊨φ → ψ. The proof proceeds by induction on the number of propositional variables occurring in φ that do not occur in ψ, denoted |atoms(φ) − atoms(ψ)|.

Base case |atoms(φ) − atoms(ψ)| = 0: Since |atoms(φ) − atoms(ψ)| = 0, we have that atoms(φ) ⊆ atoms(φ) ∩ atoms(ψ). Moreover we have that ⊨φ → φ and ⊨φ → ψ. 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. Pick a q ∈ atoms(φ) but q ∉ atoms(ψ). Now define:

φ′ := φ[⊤/q] ∨ φ[⊥/q]

Here φ[⊤/q] is the same as φ with every occurrence of q replaced by ⊤ and φ[⊥/q] similarly replaces q with ⊥. We may observe two things from this definition:

From ⊨ φ′ → φ, we have also ⊨ φ′ → ψ, so, we can apply the inductive hypothesis with χ := φ′ to obtain an interpolant φ′′ for φ′ and ψ. Because ⊨ φ → φ′, we conclude that φ′′ is also 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.

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.

Applications

Craig interpolation has many applications, among them consistency proofs, model checking, proofs in modular specifications, modular ontologies.