论带 stoup 的普世自然演绎——第一部分：命题情形

由 Gentzen 提出并经 Prawitz 深入研究的自然演绎系统是最著名的证明论框架之一。其部分成功在于自然演绎规则对逻辑常元给出了简洁刻画，尤其在直觉主义逻辑中。然而，为处理经典逻辑而对直觉主义规则集进行扩展一直饱受批评。事实上，多数此类扩展在通常的引入与消去规则之外，增添了支配否定的额外规则。其后果是若干元逻辑性质（最显著的是和谐性）丧失。Dag Prawitz 提出了一种普世自然演绎系统，将经典逻辑与直觉主义逻辑在同一系统中编码。在该系统中，经典逻辑者与直觉主义逻辑者共享全称量词、合取、否定与荒谬常元，但各自拥有含义不同的存在量词、析取与蕴涵。Prawitz 的主要思想是，这些不同含义由一套双方均可接受的语义框架给出。本文提出一种不同进路，将 Girard 的 stoup 机制适配至自然演绎框架。这将允许为 Prawitz 普世逻辑的命题片段定义一种纯和谐的天然演绎系统。