Craig interpolation
From Wikipedia, the free encyclopedia
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 ψ 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.
Contents |
[edit] 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 φ → ψ.
[edit] 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 two theories; the signature of S ∩ T is the intersection of the signatures of the two theories.
Lyndon's theorem says that if S ∪ T is unsatisfiable, then there is a 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.
[edit] Proofs of Craig interpolation
Craig interpolation can be proved with different tools:
- 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.
[edit] Applications
Craig interpolation has many applications, among them consistency proofs, model checking, proofs in modular specifications, modular ontologies.
[edit] References
- Hinman, P. (2005). Fundamentals of Mathematical Logic. A K Peters. ISBN 1-568-81262-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-0198511748.
- Eva Hoogland, Definability and Interpolation. Model-theoretic investigations. PdD 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.
