Ein Metasatz und konstruktives Verfahren, das, gegeben einen Beweis dafür, dass Formel A Formel B impliziert, eine Zwischenformel I (Interpolant) liefert, die nur die nichtlogischen Symbole benutzt, die A und B gemeinsam haben, und so dass A I impliziert und I B impliziert.

Prinzip

Ist A → B in einer Logik mit der Interpolationseigenschaft beweisbar, so existiert ein Interpolant, der ausschließlich aus dem gemeinsamen Vokabular gebildet wird; Varianten (z.B. Lyndon) schränken zusätzlich die Erhaltung der Polarität von Prädikatvorkommen ein.

Demonstration

Aussagenlogisches Beispiel: Sei A = p ∧ r und B = q ∨ r. Da A B impliziert (r macht q ∨ r wahr), ist ein Interpolant I = r: A impliziert r und r impliziert B, wobei r nur das in A und B gemeinsame atomare Symbol verwendet.

Fehlanwendung

Behaupten, ein Interpolant existiere, der beliebig gewählte gemeinsame Symbole benutzt, oder dass syntaktische Eigenschaften (z. B. Quantorstruktur oder Polarität) erhalten bleiben, in Logiken, in denen diese stärkeren Interpolationsformen nicht gelten.

Konsequenz

Ermöglicht Zerlegung von Beweisen und Übertragung von Folgen zwischen Theorien, beschränkt auf das gemeinsame Vokabular; unterstützt modulare Argumentation, Spezifikationsextraktion und automatische Verifikation.

Umkehrung

Die Umkehrung würde eine Zwischenformel verlangen, die nur nichtgemeinsames Vokabular benutzt oder gemeinsame Symbole verbietet; grundsätzlich scheitert das und widerspricht dem Zweck der Interpolation.

Abgrenzung

Gilt in vielen aussagen- und prädikatenlogischen Rahmen, kann aber in manchen Erweiterungen fehlschlagen (bestimmte Theorien mit Fixpunktoperatoren, manche modalen und höherstufigen Logiken); Gleichheit, Polarität oder theorie­spezifische Prädikate können die Existenz verhindern oder verfeinerte Varianten nötig machen.

Semantische Spannung

Spannung zwischen syntaktischer Interpolation (Interpolant aus einem Beweis konstruieren) und semantischer Interpolation (Existenz einer Formel, die Modelle trennt): Manche Logiken erlauben die eine, nicht aber die konstruktive oder polaritätserhaltende Variante.

Synthese

Craig-Interpolation ist die konstruktive Brücke, die aus einem Beweis von A → B eine Zwischenformel I extrahiert, die nur im gemeinsamen Vokabular formuliert ist, sodass A I impliziert und I B impliziert; das erlaubt modularen Informations­austausch, zeigt aber Grenzen bei störenden Vokabel-, Polaritäts- oder Logikerweiterungen.