An ecumenical notion of entailment
An ecumenical notion of entailment
复制标题
普世的蕴涵概念
DOI：
10.1007/s11229-019-02226-5
复制
发表时间：
2019
期刊：
影响因子：
1.5
通讯作者：
Valeria C V de Paiva
中科院分区：
文献类型：
--
作者：
Elaine Pimentel;L. C. Pereira;Valeria C V de Paiva
自从根岑的开创性工作以来，关于直觉主义和经典逻辑系统已经说了很多。最近，Prawitz和其他人一直在讨论如何把根岑的经典和直觉主义逻辑系统放在一个统一的系统中。我们称Prawitz的建议为普世体系，遵循佩雷拉和罗德里格斯介绍的术语。在这项工作中，我们提出了一个普世的微积分，而不是原来的自然演绎版本，并说明一些证明理论的系统属性。我们的理由是，微积分更适合广泛的调查使用的工具，证明理论，如削减消除和规则可逆性，从而允许一个完整的分析概念的合一蕴涵。然后，我们提出了一些扩展的普世教会系统，并表明，有趣的系统出现时，限制这种结石的特定片段。这种同时支持经典和直觉特征的统一系统方法不仅对逻辑本身有一定的启发，而且对它们的语义解释以及组合逻辑系统可能产生的证明理论属性也有一定的启发。
Much has been said about intuitionistic and classical logical systems since Gentzen’s seminal work. Recently, Prawitz and others have been discussing how to put together Gentzen’s systems for classical and intuitionistic logic in a single unified system. We call Prawitz’ proposal theEcumenical System, following the terminology introduced by Pereira and Rodriguez. In this work we present an Ecumenical sequent calculus, as opposed to the original natural deduction version, and state some proof theoretical properties of the system. We reason that sequent calculi are more amenable to extensive investigation using the tools of proof theory, such as cut-elimination and rule invertibility, hence allowing a full analysis of the notion of Ecumenical entailment. We then present some extensions of the Ecumenical sequent system and show that interesting systems arise when restricting such calculi to specific fragments. This approach of a unified system enabling both classical and intuitionistic features sheds some light not only on the logics themselves, but also on their semantical interpretations as well as on the proof theoretical properties that can arise from combining logical systems.