余 军 成，刘 明 元

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

余 军 成，刘 明 元

在《结构证明论》*Sara Negri & Jan von Plato. Structural Proof Theory[M]. Cambridge: Cambridge University Press, 2008.中，切割规则可容许性定理的证明在经典命题逻辑矢列演算中有四个问题：切割高度计算存在错误；“切割公式仅在左前提中是主公式”与“切割公式不是左前提的主公式”自相矛盾；收缩规则指代含混；“切割规则的任何一个前提不是逻辑公理”的表述不准确。文章分析这些问题并提出相关的解决方法，给出切割规则的可容许性定理一个详细而完整的证明，进一步论述经典命题逻辑矢列演算的子公式性质、一致性和可判定性。这些工作有助于提高学习和研究证明论的能力。

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

作者余军成，男，汉族，重庆忠县人，贵州工程应用技术学院副教授，西南大学逻辑与智能研究中心博士研究生(毕节 551700)；刘明元，男，土家族，重庆酉阳人，西南大学逻辑与智能研究中心博士研究生(北碚 400715)。

一、引言

矢列演算(sequent calculus)是关于结论及其所依赖的假设之间的可推导关系的一种形式理论[1]P85。它广泛应用于证明论、数理逻辑、计算机科学、语言学、哲学，尤其是应用于自动化证明搜索系统(systems of automatic proof search)、逻辑编程(logic programming)中。根岑(Gerhard Gentzen)于1934～1935年最早提出矢列演算系统——经典谓词逻辑演算(根岑将该系统简称为“LK”)和直觉主义谓词逻辑演算(简称为“LJ”)[2], [3]。在LK 和LJ中，“主定理”(the Hauptsatz)”即切割消去定理(the cut-elimination theorem)保证任何一个LK 或LJ推导能够转换为另一个具有相同的末矢列但没有切割(Cut)推理图模式(即切割规则)出现的LK 或LJ推导[4]P298。……