Craig interpolation

From Wikipedia, the free encyclopedia
Jump to: navigation, search

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.

Example[edit]

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[edit]

Suppose that S and T are two first-order theories. As notation, let ST denote the smallest theory including both S and T; the signature of ST is the smallest one containing the signatures of S and T. Also let ST be the intersection of the two theories; the signature of ST is the intersection of the signatures of the two theories.

Lyndon's theorem says that if ST is unsatisfiable, then there is an interpolating sentence ρ in the language of ST 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[edit]

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.

Next 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 patoms(φ) but patoms(ψ). 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:

Applications[edit]

Craig interpolation has many applications, among them consistency proofs, model checking, proofs in modular specifications, modular ontologies.

References[edit]

  1. ^ Harrison pgs. 426–427
  • John Harrison (2009). Handbook of Practical Logic and Automated Reasoning. 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.