{{Short description|Theorem in mathematical logic}} 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;<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–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> 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 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 variables occurring in φ, and ⊨ is the 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 two things from this definition:
{{NumBlk|:|{{abs|''atoms''(φ') − ''atoms''(ψ)}} {{=}} ''n''|{{EquationRef|1}}}} {{NumBlk|:|⊨ φ ↔ φ′|{{EquationRef|2}}}}
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,<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 modular specifications, modular 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