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

陈钰



基本命题逻辑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带标的矢列演算系统

公理

逻辑规则

数学规则

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

有了这个代入的定义，我们有如下引理。

证明：与内格里（S.Negri）［3］类似。

证明：与内格里（S.Negri）［3］类似。

定理3.1弱化规则：

定理3.3收缩规则：

那么，根据归纳假设有

其他联结词情况类似。

那么，根据归纳假设我们有

定理3.4切割规则：

可以转换成

其他规则类似。

可以转换成

可以转换成

其他规则类似。

可以转换成

可以转换成

其中转换后的两个前提分别由如下推演得到：

切割消去定理至此证毕。

推论3.1（弱子公式性质）在一个推演中出现的所有公式或者是最底层的矢列的子公式，或者是形如的关系原子公式。

4　结语

注释：

［1］Gabbay D M.LDS-labelled deductive systems［M］.ICON Group International，1990:11-17.

［2］Ishii K，Kashima R，Kikuchi K.Sequent calculi for Visser's propositional logics［J］.Notre Dame Journal of Formal Logic，2001（1）:1-22.

［3］Negri S，Von Plato J.Proof analysis:a contribution to Hilbert's last problem［M］.Cambridge University Press，2011:185-249.

［4］Negri S.Proof analysis in modal logic［J］.Journal of Philosophical Logic，2005（5-6）:507-544.

［5］Negri S.Proof analysis in non-classical logics［C］//Logic Colloquium.2005:107-128.

［6］Simpson A，Simpson A.The Proof Theory and Semantics of Intu-itionistic Modal Logic［D］.University of Edinburgh，1994:65-84.

［7］Suzuki Y，Ono H.Hibert style proof system for BPL［J］.Research report，1997（10）:1-8.

［8］Visser A.A propositional logic with explicit fixed points［J］.StudiaLogica，1981（2）:155-175.

Sequence Calculus System for Basic Propositional Logic

CHEN Yu
（School of Politics and Public Administration of Southwest University，Beibei，Chongqing400715，China）

A label sequence calculus G3BPLfor basic propositional logic is developed in the present paper. This system has axioms，logical rules and mathematical rule only.The structural rules are absorbed in these axioms and logical rules.In addition，all the rules of G3BPlare height-preserving invertible and the rules of weakening and contraction are height-preserving admissible.We proved the cut-elimination theorem holds for G3BPL，this system has weak sub-formula property.

Label Sequence Calculus；Basic Propositional Logic；Proof Theory.

B81

A

2096-0239（2016）03-0072-07

（责编：彭麟淋责校：明茂修）

2016-04-23

陈钰（1991- ），男，江西赣州人，西南大学政治与公共管理学院研究生。研究方向：现代逻辑。