CRAIG INTERPOLATION

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:
If
:$X$
ightarrow 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$
ightarrow Z
and
:$Z$
ightarrow Y
are tautologies, then $Z$ is called an ''interpolant'' for
:$X$
ightarrow Y.
A simple example is that of $P$ as an interpolant for
:$P$∧$R$
ightarrow P∨$Q$.
In propositional logic, the 'Craig interpolation lemma' says that whenever an implication
:$X$
ightarrow Y
is a tautology, there exists an interpolant.

Contents

Proofs of Craig interpolation

Applications

References

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.

Applications

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

References

★ Fundamentals of Mathematical Logic, Hinman, P., , , A K Peters, 2005, ISBN 1-568-81262-0

★ Interpolation and Definability: Modal and Intuitionistic Logics (Oxford Logic Guides), Dov M. Gabbay and Larisa Maksimova, , , Oxford science publications, Clarendon Press, 2006, 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.
'