Craig-Interpolation

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

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

Das Interpolationstheorem

Dieses Interpolationstheorem wurde zuerst von dem amerikanischen Logiker William Craig 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

Voraussetzung: Die Formel $A \rightarrow C$ sei ableitbar.

1. Suche alle Atome, die in A, aber nicht in C enthalten sind.
2. Für jedes dieser Atome ver-odere (Verknüpfung mit oder) A mit sich selbst, wobei jedes dieser Atome einmal mit 0 und einmal mit 1 belegt werden muss.
3. Die resultierende Formel ist die Craig-Interpolante B.

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