Constructive Semantics and the Completeness Problem

• Applicant: Dr. Thomas Piecha
• Subject Area: Theoretical Computer Science
• Term: from 2019 to 2022
• Project identifier: Deutsche Forschungsgemeinschaft (DFG) - Project number 421182908

• Final Report Year: 2023

Final Report Abstract

In constructive semantics the meaning of statements is specified in terms of the notions of proof and construction. In particular, the meaning of the logical constants is explained by determining how statements of a given logical form can be proved or inferred from other statements. Constructive semantics are the foundation of constructive logics such as intuitionistic logic and are of fundamental importance for type theory, proof assistants and the theory of programming languages. Each such semantics defines a notion of logical validity, and characterizes thus some specific constructive logic. Besides the semantic approach to logic there is the syntactical approach, in which proof systems are investigated. The completeness problem is the question whether all statements that are logically valid according to the semantics are syntactically provable in a given proof system. The main objectives of this project were to solve the completeness problem for constructive semantics and to relate our results to questions in theoretical computer science and the theory of programming languages, where constructive logics are of central importance. Although the project received only partial funding, both objectives could be reached; however, some questions could not be dealt with to the extent planned. For standard proof-theoretic semantics and intuitionistic logic we have obtained a (negative) solution of the completeness problem, and we have obtained a much better understanding of constructive semantics and the proof theory of constructive logics. Concerning the second main objective, we have improved the understanding of the relationship between constructive semantics and programming languages by studying how different meaning theories and formats of logical calculi correspond to different ways to write programs.

Publications

• 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.