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

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 that occur in logically complex statements 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, for example, so-called 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. Dag Prawitz conjectured that the completeness problem has a positive solution for a certain kind of constructive semantics and proof systems for intuitionistic logic. This conjecture is still undecided today, despite intensive research. The main objective of this project is to solve the completeness problem for constructive semantics. This kind of semantics allows for certain variations concerning the conditions for the logically complex statements on the one hand and the logically simple, so-called atomic statements on the other hand. The latter may represent factual data, defined terms or mathematical axioms, for example. Systems of rules for atomic statements, 'atomic systems' for short, are the structures or models in constructive semantics. Atomic systems may induce different kinds of derivability relations for atomic statements, yielding different notions of logical validity. To solve the completeness problem we first develop a theory of atomic systems. We then provide precise formulations of constructive semantics, and work on a solution of the completeness problem for selected semantics. We use a framework of abstract semantic conditions that will allow us to find negative solutions for concrete semantics that have specific properties. For the remaining semantics we attempt to give a completeness proof for intuitionistic logic, which would decide the completeness conjecture positively. In this case, we will have settled a long-standing open question. In the negative case, we have to solve the equally important problem of finding out which constructive logic is characterized by the considered constructive semantics. Finally, we will relate our results to further questions in theoretical computer science, in order to close certain gaps between results in proof theory and constructive logic on the one side and results obtained from the computational point of view in the theory of programming languages on the other side.

• DFG Programme: Research Grants