Craig-Interpolation

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

Es seien Fehler beim Parsen (SVG (MathML kann über ein Browser-Plugin aktiviert werden): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle T1} und Fehler beim Parsen (SVG (MathML kann über ein Browser-Plugin aktiviert werden): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle T2} zwei Theorien und der Satz Fehler beim Parsen (SVG (MathML kann über ein Browser-Plugin aktiviert werden): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle A \rightarrow C } sei ein in Fehler beim Parsen (SVG (MathML kann über ein Browser-Plugin aktiviert werden): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle T1 \cup T2 } ableitbarer Satz. Dann gilt: Es gibt ein Fehler beim Parsen (SVG (MathML kann über ein Browser-Plugin aktiviert werden): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle B} , sodass Fehler beim Parsen (SVG (MathML kann über ein Browser-Plugin aktiviert werden): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle A \rightarrow B } in Fehler beim Parsen (SVG (MathML kann über ein Browser-Plugin aktiviert werden): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle T1 } ableitbar ist, und Fehler beim Parsen (SVG (MathML kann über ein Browser-Plugin aktiviert werden): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle B \rightarrow C} ist in Fehler beim Parsen (SVG (MathML kann über ein Browser-Plugin aktiviert werden): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle 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

Voraussetzung: Die Formel Fehler beim Parsen (SVG (MathML kann über ein Browser-Plugin aktiviert werden): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle A \rightarrow C} sei ableitbar.

1. Suche alle Atome, die in Fehler beim Parsen (SVG (MathML kann über ein Browser-Plugin aktiviert werden): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle A} , aber nicht in Fehler beim Parsen (SVG (MathML kann über ein Browser-Plugin aktiviert werden): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle C} enthalten sind.
2. Für jedes dieser Atome ver-odere (Verknüpfung mit oder) Fehler beim Parsen (SVG (MathML kann über ein Browser-Plugin aktiviert werden): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle A} mit sich selbst, wobei jedes dieser Atome einmal mit Fehler beim Parsen (SVG (MathML kann über ein Browser-Plugin aktiviert werden): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle 0} und einmal mit Fehler beim Parsen (SVG (MathML kann über ein Browser-Plugin aktiviert werden): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle 1} belegt werden muss.
3. Die resultierende Formel ist die Craig-Interpolante Fehler beim Parsen (SVG (MathML kann über ein Browser-Plugin aktiviert werden): Ungültige Antwort („Math extension cannot connect to Restbase.“) von Server „https://wikimedia.org/api/rest_v1/“:): {\displaystyle 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).