View source for Craig interpolation

In [[mathematical logic]], '''Craig's interpolation theorem''' is a result about the relationship between different logical [[theory (mathematical logic)|theories]]. Roughly stated, the theorem says that if a [[well formed formula|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 (logician)|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;<ref>{{citation|title=An interpolation theorem in the predicate calculus|first=Roger|last=Lyndon|volume=9|journal=Pacific Journal of Mathematics|year=1959|pages=129–142|doi=10.2140/pjm.1959.9.129|doi-access=free}}.</ref><ref>{{citation|page=141|title=Basic Proof Theory|volume=43|series=Cambridge tracts in theoretical computer science|first1=Anne Sjerp|last1=Troelstra|author-link1=Anne Sjerp Troelstra|first2=Helmut|last2=Schwichtenberg|author-link2=Helmut Schwichtenberg|edition=2nd|publisher=Cambridge University Press|year=2000|isbn=978-0-521-77911-1}}.</ref> the overall result is sometimes called the '''Craig&ndash;Lyndon theorem'''.

== Example ==
In [[propositional logic]], let
:::<math> \varphi = \lnot(P \land Q) \to (\lnot R \land Q) </math>
:::<math> \psi = (S \to P) \lor (S \to \lnot R) </math>.

Then <math>\varphi</math> [[tautological implication|tautologically implies]] <math>\psi</math>. This can be verified by writing <math>\varphi</math> in [[conjunctive normal form]]:
:::<math>\varphi \equiv (P \lor \lnot R) \land Q</math>.

Thus, if <math>\varphi</math> holds, then <math>P \lor \lnot R</math> holds. 
:::<math>\rho = (P \lor \lnot R)</math>.

In turn, <math>P \lor \lnot R</math> tautologically implies <math>\psi</math>. Because the two propositional variables occurring in <math>P \lor \lnot R</math> occur in both <math>\varphi</math> and <math>\psi</math>, this means that <math>P \lor \lnot R</math> is an interpolant for the implication <math>\varphi \to \psi</math>.

== 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 (mathematical logic)|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]].<ref>Harrison pgs. 426–427</ref>

{{Math theorem| If ⊨φ → ψ then there is a ρ (the ''interpolant'') such that ⊨φ → ρ and ⊨ρ → ψ, where ''atoms''(ρ) ⊆ ''atoms''(φ) ∩ ''atoms''(ψ). Here ''atoms''(φ) is the set of [[propositional variable]]s occurring in φ, and ⊨ is the [[Entailment|semantic entailment relation]] for propositional logic.}}

{{Math proof|{{pipe escape|
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:

{{NumBlk|:|⊨φ' → ψ|{{EquationRef|1}}}}
{{NumBlk|:|{{abs|''atoms''(φ') − ''atoms''(ψ)}} {{=}} ''n''|{{EquationRef|2}}}}
{{NumBlk|:|⊨φ → φ'|{{EquationRef|3}}}}

This shows, then, that φ' is a suitable interplant for φ and ψ.
}}}}

Since the above proof is [[Intuitionistic logic|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 connective]]s 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 [[mu calculus|μ-calculus]], with similar complexity measures.

Craig interpolation can be proved by other methods as well.  However, these proofs are generally [[non-constructive]]:
* [[model theory|model-theoretically]], via [[Robinson's joint consistency theorem]]: in the presence of [[Compactness theorem|compactness]], negation and conjunction, Robinson's joint consistency theorem and Craig interpolation are equivalent.
* [[proof theory|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.
* [[Abstract algebraic logic|algebraically]], using [[amalgamation property|amalgamation]] theorems for the [[Variety (universal algebra)|variety]] of algebras representing the logic.
* via translation to other logics enjoying Craig interpolation.

==Applications==
Craig interpolation has many applications, among them [[consistency proof]]s, [[model checking]],<ref>{{Cite journal | last1 = Vizel | first1 = Y. | last2 = Weissenbacher | first2 = G. | last3 = Malik | first3 = S. | journal = Proceedings of the IEEE | volume = 103 | issue = 11 | year = 2015 | doi = 10.1109/JPROC.2015.2455034|title=Boolean Satisfiability Solvers and Their Applications in Model Checking| pages = 2021–2035 | s2cid = 10190144 }}</ref> proofs in [[Modularity (programming)|modular]] [[Specification language|specifications]], modular [[Ontology (computer science)|ontologies]].

==References==
<references />

==Further reading==
*{{cite book | author = John Harrison | title = Handbook of Practical Logic and Automated Reasoning |location=Cambridge, New York | publisher =[[Cambridge University Press]]| year = 2009 | isbn=978-0-521-89957-4}}
*{{cite book | author = Hinman, P. | title = Fundamentals of Mathematical Logic | publisher = A K Peters | year = 2005 | isbn = 1-56881-262-0}}
*{{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.

[[Category:Mathematical logic]]
[[Category:Lemmas]]