Constructive Semantics and the Completeness Problem

构造语义和完整性问题

• 批准号: 421182908
• 负责人: Dr. Thomas Piecha
• 金额: --
• 依托单位: Carl Friedrich von Weizsäcker-Zentrum
• 依托单位国家: 德国
• 项目类别: Research Grants
• 财政年份: 2019
• 资助国家: 德国
• 起止时间: 2018-12-31 至 2021-12-31
• 项目状态: 已结题
• 来源: https://gepris.dfg.de/gepris/projekt/421182908?language=en
• 关键词: Constructive; Semantics; Completeness; Problem

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.

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