Craig interpolation

From Wikipedia, the free encyclopedia

Depending on the type of logic being considered, the definition of Craig interpolation varies. It was first proved in 1957 for first-order logic by William Craig. Propositional Craig interpolation can be defined as follows:

$X \rightarrow Y$

is a tautology and there exists a formula $Z$ such that all propositional variables of $Z$ occur in both $X$ and $Y$ , and

$X \rightarrow Z$

and

$Z \rightarrow Y$

are tautologies, then $Z$ is called an interpolant for

$X \rightarrow Y$ .

A simple example is that of $P$ as an interpolant for

R \rightarrow P

In propositional logic, the Craig interpolation lemma says that whenever an implication

$X \rightarrow Y$

is a tautology, there exists an interpolant.

[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.