Craig-Interpolation
# 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$, sodass $A\rightarrow B$ in $T1$ ableitbar ist, und $B\rightarrow C$ ist in $T2$ 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\rightarrow C$ sei in einem korrekten Kalkül ableitbar, also tautologisch, oder, äquivalent, $A\models 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 $\bot$ und einmal durch $\top$ 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.

