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.
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, .
- Find all atoms that are in but not in .
- 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 .
- The resulting formula is the Craig interpolant .
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.
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 ).