论经典命题逻辑矢列演算的保持高度收缩定理

余军成，和宝珍



论经典命题逻辑矢列演算的保持高度收缩定理

余军成1，和宝珍2

（1.贵州工程应用技术学院逻辑与文化研究中心，贵州毕节551700；2.晋中师范高等专科学校政史系，山西晋中030600）

在《结构证明论》中，给出保持高度收缩定理在经典命题逻辑矢列演算中的一个详细而完整的证明过程，得出保持高度收缩的推论并证明了该推论，指出保持高度收缩推论在证明切割规则的可容许性定理上有减少推导步骤的作用。

经典命题逻辑矢列演算；保持高度收缩定理；保持高度收缩推论；收缩规则

1　引言

矢列演算（sequent calculus），是关于结论及其所依赖的假设之间的可推导关系的一种形式理论。［1］它在自动化证明搜索系统（systems of automatic proof search）、逻辑编程（logic programming），尤其是计算机科学、语言学、哲学中应用广泛。

经典命题逻辑矢列演算（内格里（Sara Negri）、柏拉图（Jan von Plato）将系统简称“G3cp”）的收缩规则（contraction rules）源自根岑（Gerhard Gentzen）于1935年在经典谓词逻辑演算（根岑简称“LK”）中首次提出的结构推理图模式之一［2］——收缩（contraction）［3］296。在LK中，收缩推理图模式为：

它在LK-推导以及“主要句子”（the Hauptsatz）及其推论的证明等方面有重要作用。［3］297-302

内格里和柏拉图在G3cp中给出收缩规则是可容许的（admissible）定理及部分证明过程。［4］53-54在此基础上，我们给出保持高度收缩定理一个详细而完整的证明过程，根据该证明得出保持高度收缩的推论并证明了该推论，指出保持高度收缩推论在证明切割规则的可容许性定理上有减少推导步骤的作用。

2　G3cp系统

经典命题逻辑的语言L定义如下：

逻辑公理：

逻辑规则：