Craig-Interpolation

Die Craig-Interpolation ist ein Ausdruck der Logik. Der zugrunde liegende Satz (Craig's Lemma, Interpolationstheorem) lautet folgendermaßen:
Wenn die implikative Formel $A\rightarrow C$ ableitbar ist, dann gibt es eine Interpolante B mit der Eigenschaft, dass auch die Formeln $A\rightarrow B$ und $B\rightarrow C$ ableitbar sind.

Das Interpolationstheorem

Dieses Interpolationstheorem wurde zuerst von dem amerikanischen Logiker W. Craig 1953 aufgestellt. Es wurde von S. Maehara und von K. 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, Berlin Heidelberg New York 1977