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

• Erstellungsjahr: 2023

Zusammenfassung der Projektergebnisse

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 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. Die Hauptziele dieses Projekts waren die Lösung des Vollständigkeitsproblems für konstruktive Semantiken und die Verknüpfung unserer Ergebnisse mit Fragen der theoretischen Informatik und der Theorie der Programmiersprachen, in der konstruktive Logiken von zentraler Bedeutung sind. Obwohl das Projekt nur eine Teilfinanzierung erhielt, konnten beide Ziele erreicht werden; einige Fragestellungen konnten jedoch nicht im geplanten Umfang bearbeitet werden. Für beweistheoretische (Standard-)Semantiken und intuitionistische Logik haben wir eine (negative) Lösung des Vollständigkeitsproblems erreicht und haben nun ein wesentlich besseres Verständnis von konstruktiven Semantiken und der Beweistheorie von konstruktiven Logiken. In Bezug auf das zweite Hauptziel haben wir das Verständnis der Beziehung zwischen konstruktiver Semantik und Programmiersprachen verbessert, indem wir untersucht haben, wie verschiedene Bedeutungstheorien und Formen logischer Kalküle mit verschiedenen Arten, Programme zu schreiben, korrespondieren.

Projektbezogene Publikationen (Auswahl)

• Popper on Quantification and Identity. Karl Popper's Science and Philosophy (2021), 149-169. American Geophysical Union (AGU).
  Binder, David & Piecha, Thomas
  
• "Administrative Normal Forms and Focusing for Lambda Calculi”. In: Logically Speaking. A Festschrift for Marie Duží. Ed. by Pavel Materna and Bjørn Jespersen. Vol. 49. Tributes. College Publications
  Binder, David and Thomas Piecha
  
• Data-Codata Symmetry and its Interaction with Evaluation Order
  Binder, David; Julian Jabs; Ingo Skupin & Klaus Ostermann
  
• Introduction and Elimination, Left and Right – Coq Formalization.
  Klaus Ostermann; David Binder; Ingo Skupin; Tim Süberkrüb & Paul Downen
  
• Introduction and elimination, left and right. Proceedings of the ACM on Programming Languages, 6(ICFP), 438-465.
  Ostermann, Klaus; Binder, David; Skupin, Ingo; Süberkrüb, Tim & Downen, Paul
  
• Popper’s Theory of Deductive Logic. Trends in Logic (2022), 1-79. American Geophysical Union (AGU).
  Binder, David; Piecha, Thomas & Schroeder-Heister, Peter
  
• Structural refinement types. Proceedings of the 7th ACM SIGPLAN International Workshop on Type-Driven Development (2022, 9, 6), 15-27. American Geophysical Union (AGU).
  Binder, David; Skupin, Ingo; Läwen, David & Ostermann, Klaus
  
• The Logical Writings of Karl Popper. Trends in Logic (2022). American Geophysical Union (AGU).
  Binder, David; Piecha, Thomas & Schroeder-Heister, Peter
  
• Karl Popper on Deduction. Synthese Library (2023, 12, 13), 301-321. American Geophysical Union (AGU).
  Piecha, Thomas
  
• Peter Schroeder-Heister on Proof-Theoretic Semantics. Outstanding Contributions to Logic (2024). American Geophysical Union (AGU).
  Piecha, Thomas & Wehmeier, Kai F.