Craig-Interpolation

Die Craig-Interpolation i​st ein Ausdruck d​er Logik. Der zugrunde liegende Satz (Craig’s Lemma, Interpolationstheorem) lautet folgendermaßen:

Es seien ${\displaystyle T1}$ und ${\displaystyle T2}$ zwei Theorien und der Satz ${\displaystyle A\rightarrow C}$ sei ein in ${\displaystyle T1\cup T2}$ ableitbarer Satz. Dann gilt: Es gibt ein ${\displaystyle B}$ , sodass ${\displaystyle A\rightarrow B}$ in ${\displaystyle T1}$ ableitbar ist, und ${\displaystyle B\rightarrow C}$ ist in ${\displaystyle T2}$ ableitbar.

Das Interpolationstheorem

Dieses Interpolationstheorem w​urde zuerst v​on dem US-amerikanischen Logiker William Craig (1918–2016) 1953 aufgestellt. Es w​urde von S. Maehara u​nd von Kurt Schütte (für intuitionistische Kalküle) bewiesen u​nd hat zahlreiche Anwendungen i​n der Beweis- u​nd Modelltheorie.

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

Voraussetzung: Die Formel ${\displaystyle A\rightarrow C}$ sei in einem korrekten Kalkül ableitbar, also tautologisch, oder, äquivalent, ${\displaystyle A\models C}$ .

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

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

Literatur

• 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).