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 third formula Ο, called an interpolant, such that every nonlogical 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 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
- Ο = ~(P β§ Q) β (~R β§ Q)
- Ο = (T β P) β¨ (T β ~R).
Then Ο tautologically implies Ο. This can be verified by writing Ο in conjunctive normal form:
- Ο β‘ (P β¨ ~R) β§ Q.
Thus, if Ο holds, then (P β¨ ~R) holds. In turn, (P β¨ ~R) tautologically implies Ο. Because the two propositional variables occurring in (P β¨ ~R) occur in both Ο and Ο, this means that (P β¨ ~R) is an interpolant for the implication Ο β Ο.
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.[1] 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: In this case, Ο is suitable. This is because since |atoms(Ο) β atoms(Ο)| = 0, we know 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 p β atoms(Ο) but p β atoms(Ο). Now define:
Ο' := Ο[β€/p] β¨ Ο[β₯/p]
Here Ο[β€/p] is the same as Ο with every occurrence of p replaced by β€ and Ο[β₯/p] similarly replaces p with β₯. We may observe three things from this definition:
-
β¨Ο' β Ο
(1)
-
|atoms(Ο') β atoms(Ο)| = n
(2)
-
β¨Ο β Ο'
(3)
From (1), (2) and the inductive step we have that there is an interpolant Ο such that:
-
β¨Ο' β Ο
(4)
-
β¨Ο β Ο
(5)
But from (3) and (4) we know that
-
β¨Ο β Ο
(6)
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 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,[2] proofs in modular specifications, modular ontologies.
References
- β Harrison pgs. 426β427
- β Vizel, Y.; Weissenbacher, G.; Malik, S. (2015). "Boolean Satisfiability Solvers and Their Applications in Model Checking". Proceedings of the IEEE 103 (11). doi:10.1109/JPROC.2015.2455034.
Further reading
- John Harrison (2009). Handbook of Practical Logic and Automated Reasoning. Cambridge, New York: Cambridge University Press. ISBN 0-521-89957-5.
- Hinman, P. (2005). Fundamentals of Mathematical Logic. A K Peters. ISBN 1-56881-262-0.
- Dov M. Gabbay and Larisa Maksimova (2006). Interpolation and Definability: Modal and Intuitionistic Logics (Oxford Logic Guides). Oxford science publications, Clarendon Press. 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.