Craig Interpolation

In mathematical logic, Craig's interpolation theorem is a result about the relationship between different logical theories. 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. Variants of the theorem hold for other logics, such as propositional logic. A stronger form of Craig's interpolation theorem for first-order logic was proved by Roger Lyndon in 1959; the overall result is sometimes called the Craig–Lyndon theorem.

Example

In propositional logic, let
:::$\varphi = \lnot(P \land Q) \to (\lnot R \land Q)$
:::$\psi = (S \to P) \lor (S \to \lnot R)$.

Then $\varphi$ tautologically implies $\psi$. This can be verified by writing $\varphi$ in conjunctive normal form:
:::$\varphi \equiv (P \lor \lnot R) \land Q$.
Thus, if $\varphi$ holds, then $P \lor \lnot R$ holds. In turn, $P \lor \lnot R$ tautologically implies $\psi$. Because the two propositional variables occurring in $P \lor \lnot R$ occur in both $\varphi$ and $\psi$, this means that $P \lor \lnot R$ is an interpolant for the implication $\varphi \to \psi$.

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. Formally, the theorem states:

''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 three things from this definition:

From , and the inductive step we have that there is an interpolant ρ such that:

But from and we know that

Hence, ρ is a suitable interpolant for φ and ψ.

QED

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.

References

Further reading

*
*
*{{cite book , author = Dov M. Gabbay , author2= Larisa Maksimova , author2-link= Larisa Maksimova , title = Interpolation and Definability: Modal and Intuitionistic Logics (Oxford Logic Guides) , publisher = Oxford science publications, Clarendon Press , year = 2006 , isbn = 978-0-19-851174-8
*Eva Hoogland, ''Definability and Interpolation. Model-theoretic investigations''. PhD thesis, Amsterdam 2001.
*W. Craig, ''Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory'', The Journal of Symbolic Logic 22 (1957), no. 3, 269–285.

Mathematical logic
Lemmas