Semantiken für Gödel Logiken

Logik (und Mathematik) kann als die Studie der Interaktion zwischen Syntax - Ketten von Symbolen die in andere Ketten von Symbolen transformiert werden - und Semantik - die (intendierte) Interpretation dieser Zeichenketten. Dieses war der wichtige Schritt: Die Separation dieser beiden Teile erlaubte es Logikern am Beginn des letzten Jahrhunderts Logik und Mathematik weiterzuentwickeln, wodurch sie ein goldenes Zeitalter der Mathematik einleiteten. Aber warum beschäftigen wir uns überhaupt mit Semantiken, wäre es nicht einfacher sich auf rein syntaktische Methoden zu beschränken, d.h. Methoden die automatischer Verarbeitung zugänglich sind? Dies war die Idee von Hilberts Programm am Beginn des letzten Jahrhunderts, das Erstellen eines soliden Fundamentes der Mathematik auf der Basis von rein syntaktischen Methoden und Elementen - der Traum jedes Studenten, der universelle Computer dem man eine mathematische Frage stellt und die korrekte Antwort erhält. Kurt Gödel zerstörte diese Hoffnung indem er bewies dass mit rein syntaktischen Mitteln niemals alle mathematischen Wahrheiten bewiesen werden können. Daher ist die Studie von Semantiken, besonders im Falle dass mehrere Semantiken für das gleiche syntaktische System existieren, nicht durch rein syntaktische Mitteln ersetzbar. Das Studium verschiedener Semantiken ist gleichzeitig auch eine Untersuchung der mathematischen Objekte an sich. Was wir heute `Gödel Logiken` nennen wurde aus und für die Analyse von verschiedenen mathematischen Objekten entwickelt: Die reelen Zahlen, Kripke Frames, und Heyting Algebren. Die Semantik basierend auf Teilmengen des reelen Intervals [0,1] befasst sich mit topologischen und ordnungstheoretischen Eigenschaften der reelen Zahlen. Diese Semantik wurde yum Großteil von Baaz et al. mit entscheidenden Beiträgen des Applikanten entwickelt. Kripke Frames bilden die wichtigste Semantik für Intuitionistische Logik und Modallogiken, und Untersuchungen von speziellen Kripke Frames (linear, konstante Domain) wurde größtenteils von japanischen Wissenschaftern durchgeführt. Sie können auch als Semantiken für Gödel Logiken verwendet werden, wie der Applikant im Laufe seines Marie Curie Fellowship zeigen konnte. Algebraische Semantik basierend auf speziellen Heyting Algebren wurde von Hàjek eingeführt, wobei Heyting Algebren speziellen Instanzen von Verbänden sind. Hàjek untersuchte Logiken basierend auf t-Normen als die Basis für Fuzzy Logics. Innerhalb dieser großen Klasse von t-Norm basierten Logiken gibt es drei Logiken aus denen alle anderen generiert werden können: ?ukasiewicz Logik, Produkt Logik, and Gödel Logik. Wären alle diese Semantiken gleich wäre es nutzlos sich mit ihnen zu beschäftigen. Aber während Semantiken in einem einfachen Fall (wie z.B. der propositionalen Logik) zusammenfallen können, zeigen deren Erweiterungen oft interessante Eigenschaften und Unterschiede der Semantiken. Ein typisches Beispiel ist die Klasse der endlichen Kripke Frames und die Klasse aller Kripke Frames. Die Propositionallogik der beiden Klassen ist die gleiche, während die quantifizierte Propositionallogik im ersten Fall entscheidbar ist, im zweiten aber nicht rekursiv aufzählbar. Aber auch wenn die Semantiken verschiedene Eigenschaften für verschiedene Erweiterungen aufweisen, so sind sie doch verbunden durch die gemeinsame Syntax dieser Logiken. Diese Syntax-Semantik Relation ist eine der wichtigsten in der Logik, und in der Tat kann man moderne Logik als die Geschichte dieses Zwischenspiels zwischen syntaktischen und semantischen Untersuchungen betrachten. Wir planen eine einheitliche Darstellung dieser Semantiken, einen Transfer von Ergebnissen und Techniken zwischen den Semantiken, und die Entwicklung von Kriterien bei der Untersuchung von Semantiken für mehrwertige Logiken erster Stufe.

Dieses Projekt beschäftigt sich mit Non-standard Logiken, dh Logiken die weder klassisch - zweiwertig - noch intuitionistisch sind. Innerhalb dieser Gruppe haben die Logiken die auf linear geordneten Wahrheitwertmengen basieren besondere Bedeutung und größer werdende Aufmerksamkeit erhalten, beginnend mit den frühen 20er Jahren des 20. Jahrhunderts als Lukasiewicz und Gödel die ersten Beispiel für solche Logiken einführten. Das Ziel dieses Projekt war die Untersuchung verschiedener Semantiken für Gödel Logiken, und computational interessante Fragestellungen rund um die Entscheidbarkeit der Gültigkeit und Erfüllbarkeit in diesen Logiken. Die wichtigsten Ergebnisse des Projektes betreffen die Erfüllbarkeit und Gültigkeit innerhalb verschiedener Teilklassen der Gödel Logiken. Obwohl die volle Logik erster Stufe viel zu mächtig ist um Entscheidbarkeit dieser Eigenschaften zuzulassen, können Teilklassen, die in sich stark genug sind um tatsächliche Fragestellungen zu formalisieren, trotzdem entscheidbar sein. Als Beispiel hierfür ziehe man das Monadische Fragment der Klassischen Logik heran, oder die Horn-Klasse, wichtig im Bereich der Logikprogrammierung. Möglich Unterklassen die diskutiert wurden sind die Monadische Klasse, die 1-Variablen Klasse, und weitere Fragmente spezifisch für spezielle Anwendungen. Wie in der Klassischen Logik sind Fragen die sich um die Entscheidbarkeit der Eigenschaften der Erfüllbarkeit oder Gültigkeit drehen von großer Bedeutung für tatsächliche Implementierungen und Anwendungen. Während der Projektlaufzeit wurden einige entscheidende neue Resultate auf diesem Gebiet erarbeitet. Eines dieser Resultate ist die volle Charakterisierung unter welchen Bedingungen eine monadische Gödel Logik eine entscheidbare Gültigkeit hat. Ein weiteres ist die Entscheidbarkeit eine Fragments der Gödel Logik erster Stufe das ausdrucksstark genug ist um wichtige Eigenschaften eines fuzzy Regel basierten medizinischem Expertemsystem zu modellieren. Zusammen konstituieren diese Ergebnisse einen großen Schritt vorwärts von der theoretischen Untersuchung der Gödel Logiken zu tatsächlichen Implementationen.