Die Craig-Interpolation ist ein Ausdruck der Logik. Der zugrunde liegende Satz (Craig’s Lemma, Interpolationstheorem) lautet folgendermaßen:
Es seien und zwei Theorien und der Satz sei ein in ableitbarer Satz. Dann gilt: Es gibt ein , sodass in ableitbar ist, und ist in ableitbar.
Das Interpolationstheorem Bearbeiten
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 Bearbeiten
Voraussetzung: Die Formel sei in einem korrekten Kalkül ableitbar, also tautologisch, oder, äquivalent, .
- Suche alle Atome, die in , aber nicht in enthalten sind.
- Für jedes dieser Atome ver-odere (Verknüpfung mit oder) mit sich selbst, wobei in jeder der beiden Kopien von das Atom einmal durch und einmal durch ersetzt wird.
- Die resultierende Formel ist die Craig-Interpolante .
Bei jedem Schritt wird eines der Atome, die nur in vorkommen, eliminiert. Man beachte, dass die Formel dabei exponentiell wächst – beim Bearbeiten jedes einzelnen Atoms verdoppelt sich die Größe.
Literatur Bearbeiten
- 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.