Gödellogiken: Aussagenlogische Quantoren und Parallelität

Kurt Gödel entwickelte die Gödellogiken 1933 im Zuge einer Untersuchung der intuitionistischen Logik. Diese Logiken treten auch in ganz natürlicher Weise in vielen Gebieten der Logik, Informatik und Mathematik auf. Insbesonders besteht eine enge Beziehung zwischen den Gödellogiken und bestimmten Formalisierungen der Fuzzy Logik. Die verschiedenen Gödellogiken entstehen dabei durch die Festlegung unterschiedlicher Teilmengen des Einheitsintervals [0,1] als Wahrheitwertmenge. Propositionale Gödellogiken sind vollständig analysiert: Jede unendliche Menge von Wahrheitswerten charakterisiert die gleiche Menge von Tautologien. Wenn man allerdings den Bereich der reinen Aussagenlogik verlässt, wird die Situation komplexer. Genauer gesagt kann man zwei Varianten der Quantifikation untersuchen: Quantoren erster Ordnung (All- und Existenzquantoren über Objektbereichen) und Propositional- oder Fuzzyquantoren (All- und Existenzquantoren über Aussagen). Gödellogiken erster Ordnung wurden bereits im FWF Projekt "First Order Gödel Logics" genauestens untersucht. Diese Forschung wird im Rahmen des EU Marie Curie Stipendiums "Proof Theory of First Order Fuzzy Logic" fortgesetzt. Das vorliegende Forschungsvorhaben konzentriert sich auf Propositionalquantoren, die für das Verständnis von Quantoren im allgemeinen, ihre Ausdruckskraft und ihre Beziehung zum parallelen Rechnen von entscheidender Bedeutung sind. Kurz gefasst sind die wichtigsten Ziele des vorliegenden Forschungsvorhaben - eine vollständige Charakterisierung der Gödellogiken mit propositionalen Quantoren. Insbesonders soll deren Ausdrucksstärke bestimmt werden und eine Klassifizierung gemäß topologischer Eigenschaften der Wahrheitwertmenge durchgeführt werden. - die Integration von Gödellogiken erster Ordnung und Gödellogiken mit propositionalen Quantoren (insbesonders über dem Intervall [0,1]). Die Mischlogik erlaubt zum Beispiel die Bildung von beweisbar äquivalenten Pränexformen analog zur klassischen Logik. - die Entwicklung geeigneter Interpretationen von Herleitungen in verschiedenen Formalismen der Gödellogiken (mit und ohne propositionalen Quantoren) als parallele Berechnungen.

Das Projekt hatte folgende Hauptziele: 1. eine vollständige Charakterisierung der propositionalen Gödellogiken mit Propositionalquantoren, insbesonders mit Bezug auf Ausdrucksstärke und topologische Eigenschaften der zugrundeliegenden Wahrheitswertmengen. 2. die Entwicklung von Erweiterungen von Gödellogiken erster Ordung durch Propositionalquantoren (insbesonders der Gödellogik über [0,1]) 3. geeignete Interpretationen von Ableitungen in verschiedenen Kalkülen der Gödellogiken erster Ordnung als paralelle Berechnungen. Die Projektziele wurden vollständig erreicht: eine vollständige Charakterisierung der propositionalen Gödellogiken mit Propositionalquantoren wurde durch Baaz und Preining beschrieben in Erweiterung der Analyse jener Logik, die Kripke-Strukturen des Typs w entspricht. (Die vollständige Beziehung zwischen Gödellogiken und Kripke- Strukturen wurde im Fall der ersten Ordnung durch Beckmann und Preining nachgewiesen.) Im Fall des zweiten Zieles wurde nachgewiesen, dass solche Erweiterungen ausser im Fall der endlichwertigen Gödellogiken niemals rekursiv aufzählbar sind. Das dritte Ziel wurde durch eine Konzentration auf Dialogspiele im sinne von Lorenzen erreicht, mit denen sich paralelle Abläufe in Gödellogiken sehr gut darstellen lassen. Im Rahmen des Projektes wurden zwei weitere Hauptresultate erzielt: (1) der Beweis, dass nur abzählbar viele verschiedene Gödellogiken erster Ordnung existieren. (2) die volle beweistheoretische Analyse von MTL (der Logik der halbstetigen T-Normen), eines wichtigen semantischen und syntaktischen Subsystems der Gödellogik erster Ordnung über [0,1]. Das erste Resultat ist übrraschend, da es in fast allen bekannten Fällen überabzählbar viele intermediäre Logiken gibt. Die Bedeutung des zweiten Resulates folgt aus der Tatsache, dass MTL eine der wenign Fuzzy-Logiken erster Ornung ist, die vollständig mit Bezug auf die ursprünglich intendierte Semantik ist.