Die Interpolationseigenschaft für Gödel Logiken erster Ordnung

Seit dem Erscheinen des grundlegended Resultats von Craig über Interpolation ist es offensichtlich, dass die Interpolationseigenschaft eine wesentliche Eigenschaft eines formalen Systems ist. Interpolationseigenschaften haben zahlreiche Anwendungen in der Mathematik und in der Informatik, z.B. bei Konsistenzbeweisen, Model Checking, Beweisen in modularen Spezifikationen und für modulare Ontologien. (Eine Logik L besitzt die Interpolationseigenschaft unter folgenden Umständen: immer wenn A impliziert B in L gültig ist, dann ist auch A impliziert I und I impliziert B gültig für ein I im sprachlichen Durchschnitt von A und B.) Das vorliegende Projekt soll die noch offenen Fälle der Bestimmung der Interpolationseigenschaft von Gödel Logiken erster Ordnung lösen und diese demnach im Bezug auf die Interpolationseigenschaft charakterisieren. Gödel Logiken wurden 1932 durch Gödel eingeführt um die Existenz von unendlich vielen Aussagenlogiken zwischen intuitionistischer und klassischer Aussagenlogik zu beweisen. Überschlagsmäßig können Gödel Logiken wie folgt beschrieben werden: die formale Sprache (aussagenlogisch, mit aussagelogischen Quantoren, erste Ordnung) wird wie üblich gewählt. Die Logiken sind mehrwertig und die jeweiligen Wahrheitsmengen bestehen aus abgeschlossenen Teilmengen von [0, 1], die sowohl 0 als auch 1 enthalten. 1 repräsentiert wahr. Das heißt eine Formel ist gültig, wenn sie in jeder Interpretation mit 1 bewertet wird. Konjunktion und Disjunktion berechnen sich durch Minimum und Maximum, Allquantoren und Existenzquantoren berechnen sich durch Infimum und Supremum. Der wichtigste Operator der Gödel Logiken ist die Implikation: a impliziert b berechnet sich zu 1 dann und nur dann wenn a kleiner gleich b ist, andernfalls ist der Wert b. Da die Auswertung einer Formel nur von der Anordnung, nicht aber von der Größe der verwendeten Wahrheitswerte abhängt, sind Gödel Logiken hervorragend geeignet um Vergleichbarkeit auszudrücken.

Interpolationseigenschaften sind seit dem grundlegenden Ergebnis von Craig eine der wichtigsten erwünschten Eigenschaften formaler logischer Systeme. Die Interpolation nach Craig hat zahlreiche Anwendungen in Mathematik und Informatik, zum Beispiel Konsistenzbeweise, Model-Checking, Beweisen in modularen Spezifikationen und modularen Ontologien. Zur Erinnerung: eine Logik L besitzt die Interpolationseigenschaft wenn aus der Implikation von B durch A in L auch folgt, dass eine Formel I in der gemeinsamen Sprache von A und B existiert, sodass I aus A in L folgt, und B aus I in L folgt. Dieses Projekt untersuchte das Problem der Interpolation von Gödel Logiken, insbesonders Gödel Logiken erster Ordnung. Zwei-wertige, drei-wertige, und effektive unendlich-wertige Gödel Logiken besitzen eine Form der Interpolationseigenschaft, alle anderen nicht. Die wesentlichste Einsicht, die aus diesem Projekt gewonnen werden konnte, ist die Abhängigkeit der positiven Ergebnisse von beweistheoretischen Überlegungen, insbesondere Expansionen, und der negativen Ergebnisse von modelltheoretischen Überlegungen. Expansionen entsprechen Herbrand Disjunktionen innerhalb der Formeln. Die Existenz von Herbrand Disjunktionen ist eine der wichtigsten Eigenschaften von Logiken, weil sie zeigt, dass die Logik in einem gewissen Sinn konstruktiv ist.