论文标题
在带有Stoup的普世自然扣除术中 - 第一部分：命题案例
On an ecumenical natural deduction with stoup -- Part I: The propositional case
论文作者
论文摘要
正如Prawitz提出的那样，自然扣除系统是最著名的证明理论框架之一。其成功的一部分是基于以下事实：自然扣除规则呈现出逻辑常数的简单特征，尤其是在直觉逻辑的情况下。但是，为了处理经典逻辑，对直觉主义规则的扩展存在很多批评。确实，大多数此类扩展名为通常的介绍和消除规则，额外的否定规则。结果，丢失了几种元逻辑特性，最突出的是和谐的。达格·普拉维兹（Dag Prawitz）提出了一种自然扣除式系统，其中经典的逻辑和直觉逻辑在同一系统中被编纂。在这个系统中，古典逻辑学家和直觉的逻辑学家将共享荒谬的通用量词，连词，否定和常数，但他们每个人都会有自己的存在量化者，分离和含义，并具有不同的含义。 Prawitz的主要思想是，这些不同的含义是由双方都可以接受的语义框架给出的。在本文中，我们提出了一种不同的方法，以适应自然推论框架，即吉拉德的Stoup机制。这将允许定义Prawitz的普拉维兹命题片段的纯谐自然扣除系统。
Natural deduction systems, as proposed by Gentzen and further studied by Prawitz, is one of the most well known proof-theoretical frameworks. Part of its success is based on the fact that natural deduction rules present a simple characterization of logical constants, especially in the case of intuitionistic logic. However, there has been a lot of criticism on extensions of the intuitionistic set of rules in order to deal with classical logic. Indeed, most of such extensions add, to the usual introduction and elimination rules, extra rules governing negation. As a consequence, several meta-logical properties, the most prominent one being harmony, are lost. Dag Prawitz proposed a natural deduction ecumenical system, where classical logic and intuitionistic logic are codified in the same system. In this system, the classical logician and the intuitionistic logician would share the universal quantifier, conjunction, negation and the constant for the absurd, but they would each have their own existential quantifier, disjunction and implication, with different meanings. Prawitz' main idea is that these different meanings are given by a semantical framework that can be accepted by both parties. In this paper, we propose a different approach adapting, to the natural deduction framework, Girard's mechanism of stoup. This will allow the definition of a pure harmonic natural deduction system for the propositional fragment of Prawitz' ecumenical logic.
