关于切割规则的可容许性定理的一个注释  

A Note on the Admissible Theorem of the Cut Rule

作　　者：余军成 刘明元[2] 

机构地区：[1]贵州工程应用技术学院,毕节551700 [2]西南大学逻辑与智能研究中心,北碚400715

出　　处：《贵州民族大学学报（哲学社会科学版）》2016年第5期103-117,共15页Journal of Guizhou Minzu University:Philosophy and Social Science

基　　金：中央高校基本科研业务费专项资金一般项目“达米特直觉主义逻辑演绎思想研究”[项目编号:SWU1609140];国家社会科学基金西部项目“中西方必然推理比较研究--以《九章算术》刘徽注为对象”[项目编号:11XZX009]

摘　　要：在《结构证明论》^(1)中,切割规则可容许性定理的证明在经典命题逻辑矢列演算中有四个问题:切割高度计算存在错误;"切割公式仅在左前提中是主公式"与"切割公式不是左前提的主公式"自相矛盾;收缩规则指代含混;"切割规则的任何一个前提不是逻辑公理"的表述不准确。文章分析这些问题并提出相关的解决方法,给出切割规则的可容许性定理一个详细而完整的证明,进一步论述经典命题逻辑矢列演算的子公式性质、一致性和可判定性。这些工作有助于提高学习和研究证明论的能力。In Structural Proof Theory,the proof of the admissible theorem of the cut rule in the se-quent calculus of classical propositional logic shows four problems. First,there are cut-height calculative errors. Second,it is contradictory to postulate“the cut formula is principal in the left premise only”and“the cut formula is not principal in the left premise”. Third,the referent of the contraction rule is unclear. Fourth,the expression of“none of the cut premises is an axiom”is inaccurate. This paper analyses these problems and puts forward the relevant methods to solve them,gives a detailed and complete proof of the admissible theorem of the cut rule,and further discusses the sub-formula property,consistency and decidability of the sequent calculus of classical prop-ositional logic. These jobs help to improve the ability of learning and studying proof theory. per.

关 键 词：经典命题逻辑矢列演算 切割规则的可容许性定理 子公式性质 一致性 可判定性 

分 类 号：B81[哲学宗教—逻辑学]