Craig interpolation explained

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

In propositional logic, let

\varphi=lnot(P\landQ)\to(lnotR\landQ)

\psi=(S\toP)\lor(S\tolnotR)

.

Then

\varphi

tautologically implies

\psi

. This can be verified by writing

\varphi

in conjunctive normal form:

\varphi\equiv(P\lorlnotR)\landQ

.Thus, if

\varphi

holds, then

P\lorlnotR

holds. In turn,

P\lorlnotR

tautologically implies

\psi

. Because the two propositional variables occurring in

P\lorlnotR

occur in both

\varphi

and

\psi

, this means that

P\lorlnotR

is an interpolant for the implication

\varphi\to\psi

.

Lyndon's interpolation theorem

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 languages of the two theories; the signature of ST is the intersection of the signatures of the two languages.

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

We present here a constructive proof of the Craig interpolation theorem for propositional logic.[3]

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,[4] proofs in modular specifications, modular ontologies.

References

  1. .
  2. .
  3. Harrison pgs. 426–427
  4. Vizel . Y. . Weissenbacher . G. . Malik . S. . Proceedings of the IEEE . 103 . 11 . 2015 . 10.1109/JPROC.2015.2455034. Boolean Satisfiability Solvers and Their Applications in Model Checking. 2021–2035 . 10190144 .

Further reading