Craig interpolation

The Craig interpolation is an expression of logic . The underlying theorem ( Craig's Lemma , interpolation theorem ) is as follows:

Let and two theories and the proposition be a proposition that can be derived. Then the following applies: There is a such that in is derivable, and in is derivable. ${\displaystyle T1}$ ${\displaystyle T2}$ ${\displaystyle A\rightarrow C}$ ${\displaystyle T1\cup T2}$ ${\displaystyle B}$ ${\displaystyle A\rightarrow B}$ ${\displaystyle T1}$ ${\displaystyle B\rightarrow C}$ ${\displaystyle T2}$

The interpolation theorem

This interpolation theorem was first set up in 1953 by the American logician William Craig (1918-2016). It was proven by S. Maehara and Kurt Schütte (for intuitionistic calculi) and has numerous applications in proof and model theory .

Algorithm for determining the Craig interpolant for propositional logic

Prerequisite: The formula is derived in a correct calculus, so tautological, or, equivalently, . ${\displaystyle A\rightarrow C}$ ${\displaystyle A\models C}$

1. Find all atoms that are in but not in . ${\displaystyle A}$ ${\displaystyle C}$
2. For each of these atoms ver-orere (connection with or ) with itself, whereby in each of the two copies of the atom is replaced once by and once by . ${\displaystyle p}$ ${\displaystyle A}$ ${\displaystyle A}$ ${\displaystyle p}$ ${\displaystyle \bot }$ ${\displaystyle \top }$
3. The resulting formula is the Craig interpolant . ${\displaystyle B}$

At each step, one of the atoms that can only be found in is eliminated. Note that the formula grows exponentially - when you edit each individual atom, the size doubles. ${\displaystyle A}$

literature

• Kurt Schütte : Proof Theory. Springer, Berlin et al. 1977, ISBN 3-540-07911-4 ( Basic Teachings of Mathematical Sciences 225).
• Joseph R. Shoenfield : Mathematical Logic. Addison-Wesley, Reading MA et al. 1967, ISBN 0-201-07028-6 ( Addison-Wesley Series in Logic ).