陈钰



基本命题逻辑BPLBPL带标的矢列演算系统

陈钰

（西南大学政治与公共管理学院，重庆400715）

构造基本命题逻辑BPL带标的矢列演算系统，该系统只有公理和逻辑规则，没有结构规则，结构规则被吸收在公理和逻辑规则中，并且所有的规则都是保持高度可逆的。证明弱化规则、收缩规则在中是保持高度可允许的，并证明切割消去定理，该系统具有弱子公式性质。

带标的矢列演算系统；基本命题逻辑；证明论。

1　引言

通过将蕴涵解释为形式可证，维瑟（A.Visser）提出了形式命题逻辑FPL。［8］在构造FPL之前，他首先构造了基本命题逻辑BPL，并给出了其自然演绎规则，证明其相对于传递框架是可靠的和完全的。后来，铃木（Y.Suzuki）&小野（H.Ono）给出了BPL的希尔伯特式公理化系统［7］，石井（K.Ishii）&鹿岛（R. Kashima）&菊池（K.Kikuchi）给出了其矢列演算系统，并证明了切割消去定理，而且该系统保证了子公式性质。［2］

带标的演绎系统（Labelled Deductive System）最早由加贝（D.M.Gabbay）系统提出［1］，辛普森（A.Simpson）运用这一方法从证明论的角度研究了直觉主义模态逻辑。［6］内格里（S.Negri）运用带标的演绎系统研究了模态逻辑、非经典逻辑以及中间逻辑系统。［4］［5］［3］但是，BPL作为比直觉主义逻辑更弱的逻辑，并没有得到具体的研究。因而，本文将运用这一方法，构建BPL带标的矢列演算系统，并证明其相关性质。

2　BPL的语言和语义

现在介绍铃木（Y.Suzuki）&小野（H.Ono）给出的基本命题逻辑的公理系统，它包含如下公理模式和推理规则。［7］

证明：参见［7］.

3　BPL带标的矢列演算系统

公理

逻辑规则

数学规则

下面开始讨论的一些结构性质。在讨论之前，需要引入代入的概念及其引理，这在证明的结构性质需要用到。……