Craig-Interpolation

Die Craig-Interpolation ist ein Ausdruck der Logik. Der zugrunde liegende Satz (Craig’s Lemma, Interpolationstheorem) lautet folgendermaßen:

Es seien $T 1$ und $T 2$ zwei Theorien und der Satz $A \to C$ sei ein in $T 1 \cup T 2$ ableitbarer Satz. Dann gilt: Es gibt ein $B$ , sodass $A \to B$ in $T 1$ ableitbar ist, und $B \to C$ ist in $T 2$ ableitbar.

Das Interpolationstheorem

Dieses Interpolationstheorem wurde zuerst von dem US-amerikanischen Logiker William Craig (1918–2016) 1953 aufgestellt. Es wurde von S. Maehara und von Kurt Schütte (für intuitionistische Kalküle) bewiesen und hat zahlreiche Anwendungen in der Beweis- und Modelltheorie.

Algorithmus zur Bestimmung der Craig-Interpolante für die Aussagenlogik

Voraussetzung: Die Formel $A \to C$ sei in einem korrekten Kalkül ableitbar, also tautologisch, oder, äquivalent, $A ⊨ C$ .

Suche alle Atome, die in $A$ , aber nicht in $C$ enthalten sind.
Für jedes dieser Atome $p$ ver-odere (Verknüpfung mit oder) $A$ mit sich selbst, wobei in jeder der beiden Kopien von $A$ das Atom $p$ einmal durch $⊥$ und einmal durch $⊤$ ersetzt wird.
Die resultierende Formel ist die Craig-Interpolante $B$ .

Bei jedem Schritt wird eines der Atome, die nur in $A$ vorkommen, eliminiert. Man beachte, dass die Formel dabei exponentiell wächst – beim Bearbeiten jedes einzelnen Atoms verdoppelt sich die Größe.

Literatur

William Craig, On Axiomatizability Within a System. In: The Journal of Symbolic Logic. Vol. 8 (1), March 1953: 30–32.
Kurt Schütte: Proof Theory. Springer, Berlin u. a. 1977, ISBN 3-540-07911-4 (Grundlehren der mathematischen Wissenschaften 225).
Joseph R. Shoenfield: Mathematical Logic. Addison-Wesley, Reading MA u. a. 1967, ISBN 0-201-07028-6 (Addison-Wesley Series in Logic).
Christian Thiel / Gereon Wolters: Craig's Lemma. in: Jürgen Mittelstraß: Enzyklopädie Philosophie und Wissenschaftstheorie. Zweite Auflage. Band 2, Metzler 2005.