余軍成，和寶珍

?

論經(jīng)典命題邏輯矢列演算的保持高度收縮定理

余軍成1，和寶珍2

（1.貴州工程應(yīng)用技術(shù)學(xué)院邏輯與文化研究中心，貴州畢節(jié)551700；2.晉中師范高等?？茖W(xué)校政史系，山西晉中030600）

在《結(jié)構(gòu)證明論》中，給出保持高度收縮定理在經(jīng)典命題邏輯矢列演算中的一個(gè)詳細(xì)而完整的證明過程，得出保持高度收縮的推論并證明了該推論，指出保持高度收縮推論在證明切割規(guī)則的可容許性定理上有減少推導(dǎo)步驟的作用。

經(jīng)典命題邏輯矢列演算；保持高度收縮定理；保持高度收縮推論；收縮規(guī)則

1　引言

矢列演算（sequent calculus），是關(guān)于結(jié)論及其所依賴的假設(shè)之間的可推導(dǎo)關(guān)系的一種形式理論。［1］它在自動(dòng)化證明搜索系統(tǒng)（systems of automatic proof search）、邏輯編程（logic programming），尤其是計(jì)算機(jī)科學(xué)、語言學(xué)、哲學(xué)中應(yīng)用廣泛。

經(jīng)典命題邏輯矢列演算（內(nèi)格里（Sara Negri）、柏拉圖（Jan von Plato）將系統(tǒng)簡(jiǎn)稱“G3cp”）的收縮規(guī)則（contraction rules）源自根岑（Gerhard Gentzen）于1935年在經(jīng)典謂詞邏輯演算（根岑簡(jiǎn)稱“LK”）中首次提出的結(jié)構(gòu)推理圖模式之一［2］——收縮（contraction）［3］296。在LK中，收縮推理圖模式為：

它在LK-推導(dǎo)以及“主要句子”（the Hauptsatz）及其推論的證明等方面有重要作用。［3］297-302

內(nèi)格里和柏拉圖在G3cp中給出收縮規(guī)則是可容許的（admissible）定理及部分證明過程。［4］53-54在此基礎(chǔ)上，我們給出保持高度收縮定理一個(gè)詳細(xì)而完整的證明過程，根據(jù)該證明得出保持高度收縮的推論并證明了該推論，指出保持高度收縮推論在證明切割規(guī)則的可容許性定理上有減少推導(dǎo)步驟的作用。

2　G3cp系統(tǒng)

經(jīng)典命題邏輯的語言L定義如下：

邏輯公理：

邏輯規(guī)則：

定義1：G3cp系統(tǒng)中一個(gè)推導(dǎo)或者是一個(gè)邏輯公理，或者是的一個(gè)實(shí)例（結(jié)論），或者是一個(gè)邏輯規(guī)則應(yīng)用到包含它的前提的推導(dǎo)。G3cp系統(tǒng)中一個(gè)推導(dǎo)的高度是連續(xù)應(yīng)用邏輯規(guī)則的最大數(shù)目，其中邏輯公理和的推導(dǎo)高度為0。①

3　保持高度收縮定理

在LK中，收縮推理圖模式是結(jié)構(gòu)推理圖的基本模式之一。然而，在G3cp中，沒有結(jié)構(gòu)規(guī)則，和不是G3cp的基本規(guī)則，而是導(dǎo)出規(guī)則，因此，我們需要證明收縮規(guī)則的可容許性，即保持高度收縮定理（the theorem of height-preserving contraction，簡(jiǎn)稱“Ctr-hp”）。③該定理是切割規(guī)則（the rule of cut）的可容許性定理證明的前提條件；在探討矢列演算與自然演繹（natural deduction）的關(guān)系等方面有重要作用。

證畢。

4保持高度收縮的推論

推論3（保持高度收縮的推論⑤（the corollary of height-preserving contraction，簡(jiǎn)稱“Ctr-hp*”）：對(duì)于任意的推導(dǎo)高度、公式和以及多重集合和而言，如果，那么。

在G3cp中，我們發(fā)現(xiàn)利用Ctr-hp*有助于減少切割規(guī)則可容許性定理證明過程的推導(dǎo)步驟。因?yàn)?，由“”，無論是先根據(jù)LC-hp再根據(jù)RC-hp，還是先根據(jù)RC-hp再根據(jù)LC-hp，得出結(jié)論“”的推導(dǎo)步驟需要兩步才行；然而，由“”，根據(jù)Ctr-hp*，得出結(jié)論“”的推導(dǎo)步驟僅僅需要一步就可以了。

5結(jié)論

在經(jīng)典命題邏輯矢列演算中的保持高度收縮定理，我們與內(nèi)格里和柏拉圖的不同之處在于：一是給出保持高度收縮定理一個(gè)詳細(xì)而完整的證明過程；二是根據(jù)保持高度收縮定理，得出保持高度收縮的推論并證明了該推論；三是指出保持高度收縮推論在證明切割規(guī)則的可容許性定理上有減少推導(dǎo)步驟的作用。

注釋：

①本文中加粗的“定義”、“定理”和“推論”采用順序表示法，特此說明。

②就收縮規(guī)則自身而言，LK的收縮規(guī)則與G3cp的收縮規(guī)則唯一區(qū)別在于：在前者中放置的是以逗號(hào)分隔的任意公式序列（可能是空序列）；在后者中，和是有窮的甚至可能為空的公式的多重集合。

⑤由G3cp擴(kuò)張到經(jīng)典謂詞邏輯矢列演算系統(tǒng)，該推論顯然也是成立的。

［1］Sara Negri&Jan von Plato.Proof Analysis:A Contribution to Hilbert’s Last Problem［M］.Cambridge:Cambridge University Press，2011:85.

［2］Szabo.M.E.Collected Papers of Gerhard Gentzen［M］.Amsterdam:North-Holland Publishing Company，1996:Bibliography.

［3］Gerhard Gentzen.Investigations into Logical Deduction［J］.American Philosophical Quarterly，1964（1）.

［4］Sara Negri&Jan von Plato，Structural Proof Theory［M］.Cambridge:Cambridge University Press，2008.

［5］Curry，H.B.Foundations of Mathematical Logic［M］.New York:Dover Publications Inc.，1977:173.

On the Theorem of Height-preserving Contraction in Sequence Calculus of Classical Propositional Logic inStructural Proof Theory

YU Jun-cheng1，HE Bao-zhen2

（1.Center for Logic and Culture，Guizhou University of Engineering Science，Bijie，Guizhou551700，China；2.Department of Politics and History，Jinzhong Teachers College，Jinzhong，Shanxi030600，China）

InStructural Proof Theory，this paper gives a detailed and complete proof process of the theorem of height-preserving contraction in the sequence calculus of classical propositional logic，obtains the corollary of height-preserving contraction and proofs this corollary，points out that the corollary of height-preserving contraction on the proof of admissible theorem of cut has the function of reducing the derivation steps.

Sequence calculus of Classical Propositional Logic；Theorem of Height-preserving Contraction；Corollary of Height-preserving Contraction；Contraction Rules

B81

A

2096-0239（2016）03-0059-07

（責(zé)編：彭麟淋責(zé)校：明茂修）

2016-01-15

中央高?；究蒲袠I(yè)務(wù)費(fèi)專項(xiàng)資金一般項(xiàng)目“達(dá)米特直覺主義邏輯思想演繹研究”，項(xiàng)目編號(hào)：SWU1609140；國(guó)家哲學(xué)社會(huì)科學(xué)基金重點(diǎn)項(xiàng)目“意識(shí)、表征與行動(dòng)——人類認(rèn)知的結(jié)構(gòu)與運(yùn)作機(jī)制研究”，項(xiàng)目編號(hào)：12AZD073。

余軍成（1980-），男，重慶忠縣人，貴州工程應(yīng)用技術(shù)學(xué)院邏輯與文化研究中心副教授，西南大學(xué)博士研究生。研究方向：證明論與哲學(xué)邏輯。和寶珍（1980-），女，山西文水人，晉中師范高等?？茖W(xué)校講師，碩士。研究方向：邏輯學(xué)。