Konstruktive Semantiken und das Vollständigkeitsproblem

• Antragsteller: Dr. Thomas Piecha
• Fachliche Zuordnung: Theoretische Informatik
• Förderung: Förderung von 2019 bis 2022
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 421182908

In konstruktiven Semantiken wird die Bedeutung von Aussagen mittels der Begriffe 'Beweis' und 'Konstruktion' erklärt, indem angegeben wird, wie Aussagen von bestimmter logischer Form bewiesen oder aus anderen Aussagen abgeleitet werden können. Konstruktive Semantiken sind die Grundlage konstruktiver Logiken, wie z.B. der sogenannten intuitionistischen Logik, und von grundlegender Bedeutung für die Typentheorie, Beweisassistenzsysteme und die Theorie der Programmiersprachen. Jede konstruktive Semantik legt einen Begriff der logischen Gültigkeit fest, und charakterisiert somit eine konstruktive Logik. Neben dem semantischen Ansatz gibt es in der Logik den syntaktischen Ansatz, bei dem Beweissysteme untersucht werden. Das Vollständigkeitsproblem ist die Frage, ob alle Aussagen, die gemäß einer Semantik logisch gültig sind, in einem gegebenen Beweissystem syntaktisch beweisbar sind. Dag Prawitz hat die Vermutung aufgestellt, dass das Vollständigkeitsproblem für eine bestimmte Art von konstruktiver Semantik und Beweissysteme der intuitionistischen Logik eine positive Lösung hat. Trotz intensiver Forschung ist diese Vermutung noch immer offen. Das Hauptziel dieses Projekts ist die Lösung des Vollständigkeitsproblems für konstruktive Semantiken. Bei dieser Art von Semantiken sind gewisse Variationen hinsichtlich der Bedingungen für die logisch komplexen Aussagen einerseits, und für die logisch einfachen, sogenannten atomaren Aussagen andererseits, relevant. Letztere können z.B. Faktenwissen, definierte Begriffe oder mathematische Axiome repräsentieren. Regelsysteme für atomare Aussagen, kurz 'atomare Systeme', sind die Strukturen oder Modelle in konstruktiven Semantiken. Atomare Systeme können verschiedene Arten von Ableitbarkeitsrelationen für atomare Aussagen induzieren, was zu unterschiedlichen Begriffen der logischen Gültigkeit führen kann. Zur Lösung des Vollständigkeitsproblems entwickeln wir zunächst eine Theorie atomarer Systeme. Wir geben sodann präzise Formulierungen konstruktiver Semantiken an, und arbeiten an einer Lösung des Vollständigkeitsproblems für ausgewählte Semantiken. Wir gehen dazu von gewissen abstrakten semantischen Bedingungen aus, die es uns ermöglichen, negative Lösungen für konkrete Semantiken zu finden, die bestimmte Eigenschaften aufweisen. Für die verbleibenden Semantiken versuchen wir, einen Vollständigkeitsbeweis für die intuitionistische Logik anzugeben. Ein solcher Beweis würde die Vollständigkeitsvermutung positiv entscheiden, und damit eine seit langem offene Frage beantworten. Im negativen Fall müssen wir die ebenso wichtige Frage beantworten, welche konstruktive Logik durch die jeweils betrachtete konstruktive Semantik charakterisiert ist. Schließlich werden wir unsere Ergebnisse auf weitere Fragen der theoretischen Informatik anwenden, um Lücken zwischen Resultaten der Beweistheorie und der konstruktiven Logik einerseits und der Theorie der Programmiersprachen andererseits zu schließen.

• DFG-Verfahren: Sachbeihilfen