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.