關于切割規則的可容許性定理的一個注釋*

余 軍 成，劉 明 元

關于切割規則的可容許性定理的一個注釋*

余 軍 成，劉 明 元

在《結構證明論》*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。它是矢列演算的核心結論，顯示了建立矢列演算系統的重要性，對包括一致性等元理論成果具有深遠的影響。因此，根岑給出了該定理的完整證明過程[5]P298-306。在LK 和LJ推導中，一方面，切割消去定理保證能夠根據子公式性質(the subformula property)從根部(root)出發向上進行證明搜索；另一方面，正如布洛斯(George Boolos)所言，應用切割規則會極大地減少推導的長度[6]。

根岑的學生凱托寧[7](Oiva Ketonen)、克萊尼[8]P453(Stephen Cole Kleene)、柯里[9]P208-213(Haskell Brooks Curry)、內格里(Sara Negri)和柏拉圖(Jan von Plato)[10]P25-60等在LK 和LJ的基礎上，提出經典邏輯和直覺主義邏輯的矢列演算的各種變形系統。他們所提出的各種變形系統的邏輯規則與根岑提出的矢列演算系統的邏輯規則有很大的不同：在LK 和LJ中，并非所有的邏輯規則都是可逆的(invertible)。在經典命題邏輯矢列演算中，這些變形系統既有一個共同點：所有邏輯規則是可逆的并且都具有子公式性質；也有一個不同點：從有結構規則向沒有結構規則轉變。在有切割規則的變形系統中需要證明切割消去定理；在沒有切割規則的變形系統中需要證明切割規則是可容許的(admissible)，即切割規則的可容許性定理。因此，有切割規則的矢列演算與沒有切割規則的矢列演算如果兩者是等價的，那么切割消去定理與切割規則的可容許性定理兩者的作用是相同的。然而，在經典命題邏輯矢列演算變形系統中，凱托寧、克萊尼、柯里，內格里和柏拉圖僅僅給出切割消去定理或切割規則的可容許性定理的部分證明，其中，內格里和柏拉圖的證明較為詳盡而易于接受[11]P54-57。在內格里和柏拉圖的基礎上，我們指出經典命題邏輯矢列演算系統(簡稱“G3cp*“G”是“甘岑系統”的縮寫，“3”表示“沒有結構規則”，“cp”是“經典命題邏輯”的縮寫，“ip”是“直覺主義命題邏輯”的縮寫?！?[12]P60中切割規則的可容許性定理證明有四個問題，我們分析了這些問題且提出相關的解決方法，給出切割規則的可容許性定理一個完整而詳盡的證明，進一步論述了G3cp的子公式性質、一致性和可判定性。

二、G3cp系統

經典命題邏輯的語言L定義如下：

通過P, Q, R, … 表示的原子公式是公式，以及通過⊥表示的恒假是公式；如果A和B是公式，那么A∧B, A∨B, A?B是公式，此外，A=def(A?⊥)并且A??B=def(A?B)∧(B?A)。

在G3cp中，矢列式的形式為Γ?Δ，其中，Γ和Δ是有窮的甚至可能為空的公式的多重集合(multisets)；其邏輯公理和邏輯規則如下所示[13]P49。

邏輯公理：

P,Γ?Δ,P

邏輯規則：

定義1*本文中加粗的“定義”、“定理”和“推論”采用順序表示法，特此說明。：一個公式A的權重(weight)(簡稱“w(A)”)通過如下方式歸納定義，w(⊥)=0；對于原子公式P，w(P)=1；w(A∧B)=w(A∨B)=w(A?B)=w(A)+w(B)+1。

定義2：在G3cp系統中，一個推導或者是一個邏輯公理，或者是L⊥的一個實例(結論)，或者是一個邏輯規則應用到包含它的前提的推導；一個推導的高度是連續應用邏輯規則的最大數目，其中，邏輯公理和L⊥的推導高度為0。

說明：在G3cp系統中，對于任意的公式A、多重集合Γ和Δ，矢列式A,Γ?Δ,A是可推導的[14]P30-31；“nΓ?Δ”表示在推導高度至多為n時，矢列式Γ?Δ是可推導的；弱化規則和收縮規則是導出規則，都是保持高度可推導的[15]P53-54。

三、切割規則的可容許性定理證明存在的問題

在G3cp系統中沒有結構規則，自然就沒有切割規則，因而不需要證明切割消去定理。一個自然而然的問題：在G3cp系統中，為什么我們需要證明切割規則是可容許的呢？因為在我們的推理中，經常采用合成的證明，其中我們使用輔助的結論，它有助于我們縮短證明的過程。切割規則只不過是這種利用輔助結論的正式的對應物，它允許我們以正規的方式繼續使用輔助引理[16]P24，從而極大地降低推導的高度。切割規則在G3cp系統中表現形式：

因此，需要證明該規則在G3cp系統中是可容許的；而且，我們發現內格里和柏拉圖關于切割規則的可容許性定理證明存在以下四個問題：

(一)切割高度*在一個推導中切割規則的一個實例的切割高度(Cut-height)是該切割規則的兩個前提的推導高度之和。計算存在錯誤

在“切割公式D在兩個前提中是主公式”的兩種子情況的證明過程中，出現了切割高度計算存在錯誤的問題。因為“與轉換前的切割推導相比，轉換后有較低切割高度的兩個切割推導”[17]P56-57與“在其中切割公式在切割的兩個前提中不是主公式的所有情況下，切割高度是減少的”以及“向上的切割排列不是一直減少切割高度而是可以增加它”[18]P35顯然前后自相矛盾。如果詳細計算切割高度，我們將會發現：轉換后上面的一個切割的切割高度比轉換前的切割高度減少；轉換后下面的一個切割的切割高度與轉換前的切割高度則無法精確比較究竟是減少還是增加。因而，證實了切割高度計算存在錯誤的問題。

(二)“切割公式僅在左前提中是主公式”與“切割公式不是左前提的主公式”自相矛盾

當“切割公式D僅在左前提中是主公式”時，我們需要考慮的是如何減少右前提D,?！?Δ′的推導高度。已知切割公式D不是右前提的主公式，因而，右前提的主公式要么在Γ′中，要么在Δ′中?！瓣P于Δ=A?B,Δ′的L?”和“關于Δ=A∨B,Δ″的R∨”[19]P56顯然指的是“左前提Γ?Δ,D的主公式在Δ中”(如果主公式在Δ中，則Δ=A?B,Δ′的L?規則顯然是有問題的，因為Δ是左前提的后件，不可能是L?規則，而且Δ′與右前提的后件相互混淆。如果主公式在Γ中，那么有L?規則，但是，矢列式“Δ=A?B,Δ′”應改寫為“Γ=A?B,Γ″”。因此，無論如何，“關于Δ=A?B,Δ′的L?”，要么規則運用有誤，要么矢列式寫法有誤。此處，先撇開這兩個錯誤)，即“切割公式D不是左前提的主公式”，顯然與“切割公式D僅在左前提中是主公式”自相矛盾。

(三)收縮規則指代含混

在“切割公式D在兩個前提中是主公式”的兩種子情況*如果內格里和柏拉圖呈現第一種子情況的證明，同樣會出現收縮規則指代含混的問題。的證明過程中，還出現了收縮規則(簡稱“Ctr”)指代含混的問題。因為，Ctr規則是直覺主義命題邏輯矢列演算(簡稱“G3ip”)的導出規則：

在G3cp中，導出的收縮規則為：

收縮規則在G3ip和G3cp中顯然是不同的，不能混用。因此，在G3cp中，關于“這兩種子情況的證明過程”不可能會應用到G3ip導出的收縮規則“Ctr”，我們需要用“LC和RC”替換“Ctr”，否則，混用或者亂用收縮規則的現象將無法避免。

(四)“切割規則的任何一個前提不是邏輯公理”的表述不準確

除“切割規則的任何一個前提(即左前提和右前提)不是邏輯公理”之外，還應該包括“不是L⊥的結論”。因為它是與“切割規則的左前提是一個邏輯公理或L⊥的結論”以及“切割規則的右前提是一個邏輯公理或L⊥的結論”不同的第三種情況，這種情況顯然不可能與前面兩種情況有重合之處；在第三種情況的證明過程中，需要詳細計算切割高度與L⊥的結論的推導高度為0(不需要計算切割高度)相矛盾?；谶@兩點理由，我們很容易斷定內格里、柏拉圖關于“切割規則的任何一個前提不是邏輯公理”的表述不準確，遺漏了“不是L⊥的結論”。

四、切割規則的可容許性定理的證明

定理3：切割規則，

在G3cp中是可容許的。它是該系統最重要的定理，因此需要詳細考察該定理的證明過程。為了更好地解決以上四個問題，我們將給出一個詳細而完整的切割規則的可容許性定理的證明。

證明：假定任給一個推導*假定推導的最上層矢列式從左到右的推導高度分別為n、m、k、…。的最后一步所應用的規則是切割規則，此外該推導中不再包含其他的切割規則，我們可以將該推導轉換為一個具有相同結論但不包含切割規則的推導。對切割公式的權重以及子推導切割高度進行歸納。

我們首先要區分兩種情況：一是切割規則的前提是邏輯公理或者L⊥的結論。二是切割規則的前提不是邏輯公理或L⊥的結論。然后再分別討論兩種情況的子情況，直至討論完所有可能的子情況。

(一)切割規則至少有一個前提是一個邏輯公理或者L⊥的結論

1.切割的左前提Γ?Δ,D是一個邏輯公理或L⊥的結論

我們區分了三種子情況：一是切割公式D在Γ中。對右前提D,Γ′?Δ′運用弱規則(既包括左邊的弱規則也包括右邊的弱規則)可推導出Γ,?！?Δ,Δ′。

二是Γ和Δ含有相同的原子公式。那么，Γ,Γ′?Δ,Δ′也是一個邏輯公理。

三是⊥在Γ中。那么，Γ,Γ′?Δ,Δ′同樣是一個L⊥的結論。

2.切割的右前提D,?！?Δ′是一個邏輯公理或L⊥的結論

二是?！浜挺ぁ浒ㄏ嗤脑庸?。那么，Γ,?！?Δ,Δ′也是一個邏輯公理。

三是⊥在?！渲?。那么，Γ,?！?Δ,Δ′同樣是一個L⊥的結論。

四是D=⊥。我們對左前提又區分了兩種情況：(1)Γ?Δ,⊥是一個邏輯公理或L⊥的結論。那么，或者Γ和Δ含有相同的原子公式，或者⊥在Γ中，因此，Γ,?！?Δ,Δ′同樣是一個邏輯公理或L⊥的結論。

(2)它是可推導的?！筒豢赡苁亲笄疤幡?Δ,⊥的主公式，因此，主公式要么在Γ中，要么在Δ中。我們又可以區分六種情況：Γ=A∧B,?！澹沪?A∨B,Γ″；Γ=A?B,Γ″；Δ=Δ″,A∧B；Δ=Δ″,A∨B；Δ=Δ″,A?B。

當Γ=A∧B,Γ″時，推導

A,B,?！?Δ,⊥L∧

轉換為推導

1.發揮資源優勢，做強冰雪旅游產業。冰雪旅游業是冰雪產業的主體，發展冰雪產業，首先要做強冰雪旅游業。吉林省應以冰雪資源優勢為基礎，以長吉都市、長白山、查干湖地區為中心，結合地域特色，實現錯位有序發展，建成“一山、兩城、三區”的冰雪旅游產業空間發展布局，構建知名冰雪產業品牌。

A,B,?！?Δ,⊥ ⊥,Γ′?Δ′Cut(n)

當Γ=A∨B,Γ″時，推導

A,?！?Δ,⊥ B,?！?Δ,⊥L∨

轉換為推導

當Γ=A?B,Γ″時，推導

?！?Δ,⊥,A B,?！?Δ,⊥L?

轉換為推導

當Δ=Δ″,A∧B時，推導

Γ?Δ″,A,⊥Γ?Δ″,B,⊥R∧

轉換為推導

當Δ=Δ″,A∨B時，推導

Γ?Δ″,A,B,⊥R∨

轉換為推導

當Δ=Δ″,A?B時，推導

A,Γ?Δ″,B,⊥R?

轉換為推導

(二)切割規則沒有前提是邏輯公理或者L⊥的結論

1.切割公式D在左前提Γ?Δ,D中不是主公式

在這種情況下，左前提的主公式要么在Γ中，要么在Δ中。我們可以區分六種情況：Γ=A∧B,?！?；Γ=A∨B,Γ″；Γ=A?B,?！?；Δ=Δ″,A∧B；Δ=Δ″,A∨B；Δ=Δ″,A?B。

當Γ=A∧B,?！鍟r，推導

A,B,?！?Δ,DL∧

轉換為推導

當Γ=A∨B,?！鍟r，推導

A,Γ″?Δ,D B,?！?Δ,DL∨

轉換為推導

當Γ=A?B,?！鍟r，推導

Γ″?Δ,D,A B,Γ″?Δ,DL?

轉換為推導

當Δ=Δ″,A∧B時，推導

Γ?Δ″,A,DΓ?Δ″,B,DR∧

轉換為推導

當Δ=Δ″,A∨B時，推導

Γ?Δ″,A,B,DR∨

轉換為推導

當Δ=Δ″,A?B時，推導

A,Γ?Δ″,B,DR?

轉換為推導

2.切割公式D僅在左前提中是主公式

切割公式D在右前提D,Γ′?Δ′中不是主公式，右前提的主公式要么在Γ′中，要么在Δ′中。我們可以區分六種情況：Γ′=A∧B,Γ″；Γ′=A∨B,Γ″；?！?A?B,?！澹沪ぁ?Δ″,A∧B；Δ′=Δ″,A∨B；Δ′=Δ″,A?B。

當?！?A∨B,?！鍟r，推導

D,A,B,Γ″?Δ′L∧

轉換為推導

當?！?A∨B,?！鍟r，推導

D,A,Γ″?Δ′ D,B,?！?Δ′L∨

轉換為推導

當Γ′=A?B,?！鍟r，推導

D,?！?Δ′,A D,B,?！?Δ′L?

轉換為推導

當Δ′=Δ″,A∧B時，推導

D,?！?Δ″,A D,?！?Δ″,BR∧

轉換為推導

當Δ′=Δ″,A∨B時，推導

D,?！?Δ″,A,BR∨

轉換為推導

當Δ′=Δ″,A?B時，推導

D,A,?！?Δ″,BR?

轉換為推導

3.切割公式D在左前提和右前提中都是主公式

我們區分為三種情況：D=A∧B；D=A∨B；D=A?B。

當D=A∧B時，推導

轉換為推導

Γ?Δ,A A,B,Γ′?Δ′Cut(n+k)

當D=A∨B時，推導

轉換為推導

Γ?Δ,A,B B,?！?Δ′Cut(n+k)

當D=A?B時，推導

轉換為推導

?！?Δ′,A A,Γ?Δ,BCut(m+n)

五、G3cp系統的推論

推論4：在G3cp中，關于矢列式在Γ?Δ推導中的所有公式是Γ和Δ的子公式[21]P57。因為G3cp沒有結構規則，通過觀察它的邏輯公理和邏輯規則，可以立即得出這一推論。

在證明論語義[22]的幾種方法中，子公式性質是一種重要性質：如果矢列式Γ?Δ是可推導的且有切割消去定理作為保障，那么從根部出發利用邏輯規則向上進行證明搜索，一定存在這樣一個推導，它的所有分支的最上層矢列式一定是邏輯公理或者L⊥的結論，而且推導中的所有公式是Γ和Δ的子公式。與有結構規則的經典命題邏輯矢列演算系統相較，G3cp系統一方面更適合自動證明搜索，因為它沒有切割規則但同樣具有子公式性質；另一方面切割規則的可容許性定理同樣不僅可以簡化向上證明搜索的步驟，而且針對同一邏輯的不同邏輯系統之間元理論的比較研究有至關重要的作用。

此外，如果一個系統承認關于“?”(或者⊥)的一個證明，那么該系統顯然不具有一致性。因為，如果該系統有切割消去定理，那么關于“?”的證明就可以轉化為不使用切割規則的“?”的證明，通過觀察該系統的邏輯公理、邏輯規則以及不包括切割規則的其他結構規則，將會發現沒有任何一個關于“?”的證明，這與承認有關于“?”的一個證明自相矛盾。在G3cp中，當Γ和Δ為空的多重集合時，“?”同樣是不可推導的。因為，“?”既不是一個邏輯公理，也沒有任何邏輯規則可以推導出它，也就是說，G3cp語形上是一致的。而且，關于任意一個矢列式Γ?Δ是不是可推導的，在G3cp中是可判定的：在一般的情況下，在G3cp中如果矢列式Γ?Δ是不可推導的，那么從根部出發利用邏輯規則向上進行證明搜索，關于它的所有可能的推導，其中，任何一個推導一定存在某個分支的最上層矢列式既不是邏輯公理也不是L⊥的結論；反之，則是可推導的。如果根據引理：在G3cp中，從矢列式Γ?Δ到最上層矢列式的分解是唯一的[23]P51，那么，如果它的最上層矢列式是邏輯公理或者L⊥的結論，則是可推導的；如果它的最上層矢列式既不是邏輯公理也不是L⊥的結論，則是不可推導的。因此，與一般情況相較，利用這個引理的優勢在于，它可以大大簡化如果矢列式Γ?Δ是不可推導的判定程序。

六、結語

在G3cp系統中，我們與內格里、柏拉圖的不同之處在于：一是指出切割規則的可容許性定理證明存在四個問題；二是分析這些問題并提出相關的解決方法；三是給出切割規則的可容許性定理一個詳細而完整的證明；四是進一步論述經典命題邏輯矢列演算的子公式性質、一致性和可判定性。這些工作有助于提高學習和研究證明論的能力。

[1]Sara Negri & Jan von Plato. Proof Analysis: A Contribution to Hilbert’s Last Problem[M]. Cambridge: Cambridge University Press, 2011.

[2]Gerhard Gentzen. Untersuchungen über das logische Schlie?en. I[J]. Mathematische Zeitschrift,1934,39,(2).

[3]Gerhard Gentzen. Untersuchungen über das logische Schlie?en. II[J]. Mathematische Zeitschrift,1935,39,(3).

[4][5]Gerhard Gentzen. Investigations into Logical Deduction[J]. American Philosophical Quarterly,1964,1.

[6]George Boolos. Don't Eliminate Cut[J]. Journal of Philosophical Logic, 1984,13,(4).

[7]Oiva Ketonen. Untersuchungen zum Pr?dikatenkalkül[D]. Helsinki, Annales Academiae Scientiarum Fennicae, Series A, I. Mathematica-physica,1944,23.

[8]Kleene, S. C. Introduction to Metamathematics[M]. Amsterdam: North-Holland Publishing Company, 1952.

[9]Curry, H. B. Foundations of Mathematical Logic[M]. New York: Dover Publications Inc, 1977.

[10][11][13][14][15][17][18][19][21][23]Sara Negri & Jan von Plato. Structural Proof Theory[M]. Cambridge: Cambridge University Press, 2008.

[12]Troelstra, A. S. and H. Schwichtenberg. Basic Proof Theory[M]. Cambridge: Cambridge University Press, 2000.

[16]Francesca Poggiolesi. Gentzen Calculi for Modal Propositional Logic[M]. Berlin: Springer, 2011.

[20]Hodes, H. T. Review[J]. The Philosophical Review,2006,115,(2).

[22]Reinhard Kahle and Peter Schroeder-Heister. Introduction: Proof-Theoretic Semantics[J]. Synthese, 2006.

責任編輯：陳 剛

ANoteontheAdmissibleTheoremoftheCutRule

YU Juncheng,LIU Mingyuan

In Structural Proof Theory, the proof of the admissible theorem of the cut rule in the sequent 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 subformula property, consistency and decidability of the sequent calculus of classical propositional logic. These jobs help to improve the ability of learning and studying proof theory.per

sequent calculus of classical propositional logic; admissible theorem of the cut rule; sub-formula property; consistency; decidability

B81

A

1003-6644(2016)05-0103-15

* 中央高校基本科研業務費專項資金一般項目“達米特直覺主義邏輯演繹思想研究”[項目編號：SWU1609140]；國家社會科學基金西部項目“中西方必然推理比較研究——以《九章算術》劉徽注為對象”[項目編號：11XZX009]。 * 郭美云教授閱讀了全文，并指出文章的標題及引言的修改意見，特此致謝。