Constructive Semantics and the Completeness Problem

在构造性语义学中，陈述的意义是用证明和构式的概念来规定的。特别是，通过确定如何从其他语句中证明或推断给定逻辑形式的语句，来解释出现在逻辑复杂语句中的逻辑常量的含义。构造性语义学是构造性逻辑的基础，例如所谓的直觉主义逻辑，并且对于类型理论、证明助手和程序设计语言理论是基本重要的。每一个这样的语义学都定义了一个逻辑有效性的概念，并因此表征了一些特定的建构性逻辑。除了逻辑的语义方法外，还有句法方法，在这种方法中，证明系统被研究。完备性问题是根据语义逻辑有效的所有陈述在给定的证明系统中是否在句法上可证明的问题。Dag Prawitz猜想，对于某种构造性语义和直觉逻辑的证明系统，完备性问题有一个正解。尽管进行了大量研究，但这一猜测至今仍未确定。这个项目的主要目标是解决构造性语义的完备性问题。这种语义允许关于逻辑上复杂的语句和逻辑上简单的所谓原子语句的条件的某些变化。例如，后者可以表示事实数据、定义的术语或数学公理。原子语句规则体系，简称原子系统，是构造性语义学中的结构或模型。原子系统可能会为原子语句归纳出不同类型的派生关系，从而产生不同的逻辑有效性概念。为了解决完备性问题，我们首先发展了原子系统理论。然后，我们提供了构造性语义的精确公式，并致力于解决所选语义的完备性问题。我们使用抽象语义条件的框架，这将允许我们为具有特定属性的具体语义找到否定的解决方案。对于剩下的语义，我们试图给出直觉主义逻辑的完备性证明，这将肯定地决定完备性猜想。在这种情况下，我们将解决一个长期悬而未决的问题。在否定的情况下，我们必须解决同样重要的问题，即找出哪个构造逻辑以所考虑的构造语义为特征。最后，我们将把我们的结果与理论计算机科学中的进一步问题联系起来，以便一方面弥合证明论和构造逻辑中的结果与程序设计语言理论中从计算角度获得的结果之间的某些差距。

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.