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;[1][2] the overall result is sometimes called the Craig–Lyndon theorem.
Example
editIn propositional logic, let
- ?
- ?.
Then ? tautologically implies ?. This can be verified by writing ? in conjunctive normal form:
- ?.
Thus, if ? holds, then ? holds.
- ?.
In turn, ? tautologically implies ?. Because the two propositional variables occurring in ? occur in both ? and ?, this means that ? is an interpolant for the implication ?.
Lyndon's interpolation theorem
editSuppose 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
editWe present here a constructive proof of the Craig interpolation theorem for propositional logic.[3]
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.
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:
| ?φ' → ψ | 1 |
| |atoms(φ') ? atoms(ψ)| = n | 2 |
| ?φ → φ' | 3 |
This shows, then, that φ' is a suitable interplant 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
editCraig interpolation has many applications, among them consistency proofs, model checking,[4] proofs in modular specifications, modular ontologies.
References
edit- ^ Lyndon, Roger (1959), "An interpolation theorem in the predicate calculus", Pacific Journal of Mathematics, 9: 129–142, doi:10.2140/pjm.1959.9.129.
- ^ Troelstra, Anne Sjerp; Schwichtenberg, Helmut (2000), Basic Proof Theory, Cambridge tracts in theoretical computer science, vol.?43 (2nd?ed.), Cambridge University Press, p.?141, ISBN?978-0-521-77911-1.
- ^ 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): 2021–2035. doi:10.1109/JPROC.2015.2455034. S2CID?10190144.
Further reading
edit- John Harrison (2009). Handbook of Practical Logic and Automated Reasoning. Cambridge, New York: Cambridge University Press. ISBN?978-0-521-89957-4.
- Hinman, P. (2005). Fundamentals of Mathematical Logic. A K Peters. ISBN?1-56881-262-0.
- Dov M. Gabbay; 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.