Craig interpolation

From Wikipedia, the free encyclopedia

Depending on the type of logic being considered, the definition of Craig interpolation varies. Propositional Craig interpolation can be defined as follows:

If

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

and

are tautologies, then Z is called an interpolant for

.

A simple example is that of P as an interpolant for

P∧∨Q.

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

is a tautology, there exists an interpolant.

[edit] References

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