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:

Applications

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

References

  1. ↑ Harrison pgs. 426–427
  2. ↑ 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

This article is issued from Wikipedia - version of the Thursday, October 29, 2015. The text is available under the Creative Commons Attribution/Share Alike but additional terms may apply for the media files.