Gödel Logiken: prenexe Fragmente

Die Existenz logisch equivalenter prenexer Formen ist eine der ältesten beobachteten Eigenschaften der klassischen Logik erster Ordnung. Diese prenexen Formen werden in uneindeutiger Weise durch das Verschieben von Quantoren erzeugt. Prenexe Formen sind die Grundlage von Herbrands Theorem, und infolgedessen des automatischen Beweisens (Herbrands Theorem ist die Feststellung, dass eine gültige Existenzformel einer aussagenlogisch gültigen Disjunktion entspricht.). In diesem Projekt soll die Beziehung von Gödel Logiken zu den jeweiligen prenexen Fragmenten charakterisiert werden. Gödel Logiken wurden 1932 durch Gödel begründet um den Nachweis zu erbringen, dass es abzählbar viele Aussagenlogiken zwischen intuitionistischer und klassischer Aussagenlogik gibt. Grob gesprochen können Gödel Logiken wie folgt beschrieben werden. Die Sprache ist eine Standard (aussagenlogische, quantifiziert-logische, prädikatenlogische) Sprache. Die Logiken sind mehrwertig, und die Mengen der Wahrheitswerte sind (abgeschlossene) Teilmengen von [0,1], welche sowohl 0 als auch 1 enthalten. 1 ist der ausgezeichnete Wert, d.h. eine Formel ist gültig, wenn sie den Wert 1 in jeder Interpretation erhält. Die Wahrheitsabbildungen der Konjunktion und Disjunktion sind Minimum und Maximum, und in der Prädikatenlogik sind die Quantoren durch Infimum und Supremum bestimmt. Der charakteristische Operator der Gödel Logiken, die Gödel Implikation, ist definiert durch: A impliziert B ist wahr, wenn A kleiner gleich B ist, und A impliziert B ist B in allen anderen Fällen. Da die Bewertung einer Formel nur von der Anordnung, aber nicht von der Größe der Wahrheitswerte abhängt, sind Gödel Logiken geeignet um Vergleiche formal wiederzugeben. Gödel Logiken sind auch Logiken zwischen intuitionistischer und klassischer Logik, welche durch endliche, oder abzählbare linear geordnete Kripke Strukturen mit gleichbleibendem Objektbereich spezifiziert werden. Die prenexen Fragmente von Gödel Logiken lassen Skolemisierung zu, und sind infolgedessen die Grundlage angemessener automatischer Beweisverfahren. Zusätzlich erlauben die prenexen Fragmente Herbrands Theorem, zumindest in approximativen Varianten. Sie dienen auch der Suche nach prenexen Normalformen, die dazu verwendet werden um die Komplexität bestimmter Gödel Logiken zu bestimmen.