余 軍 成，劉 明 元

關(guān)于切割規(guī)則的可容許性定理的一個注釋*

余 軍 成，劉 明 元

在《結(jié)構(gòu)證明論》*Sara Negri & Jan von Plato. Structural Proof Theory[M]. Cambridge: Cambridge University Press, 2008.中，切割規(guī)則可容許性定理的證明在經(jīng)典命題邏輯矢列演算中有四個問題：切割高度計算存在錯誤；“切割公式僅在左前提中是主公式”與“切割公式不是左前提的主公式”自相矛盾；收縮規(guī)則指代含混；“切割規(guī)則的任何一個前提不是邏輯公理”的表述不準(zhǔn)確。文章分析這些問題并提出相關(guān)的解決方法，給出切割規(guī)則的可容許性定理一個詳細(xì)而完整的證明，進(jìn)一步論述經(jīng)典命題邏輯矢列演算的子公式性質(zhì)、一致性和可判定性。這些工作有助于提高學(xué)習(xí)和研究證明論的能力。

經(jīng)典命題邏輯矢列演算；切割規(guī)則的可容許性定理；子公式性質(zhì)；一致性；可判定性

作者余軍成，男，漢族，重慶忠縣人，貴州工程應(yīng)用技術(shù)學(xué)院副教授，西南大學(xué)邏輯與智能研究中心博士研究生(畢節(jié) 551700)；劉明元，男，土家族，重慶酉陽人，西南大學(xué)邏輯與智能研究中心博士研究生(北碚 400715)。

一、引言

矢列演算(sequent calculus)是關(guān)于結(jié)論及其所依賴的假設(shè)之間的可推導(dǎo)關(guān)系的一種形式理論[1]P85。它廣泛應(yīng)用于證明論、數(shù)理邏輯、計算機(jī)科學(xué)、語言學(xué)、哲學(xué)，尤其是應(yīng)用于自動化證明搜索系統(tǒng)(systems of automatic proof search)、邏輯編程(logic programming)中。根岑(Gerhard Gentzen)于1934～1935年最早提出矢列演算系統(tǒng)——經(jīng)典謂詞邏輯演算(根岑將該系統(tǒng)簡稱為“LK”)和直覺主義謂詞邏輯演算(簡稱為“LJ”)[2], [3]。在LK 和LJ中，“主定理”(the Hauptsatz)”即切割消去定理(the cut-elimination theorem)保證任何一個LK 或LJ推導(dǎo)能夠轉(zhuǎn)換為另一個具有相同的末矢列但沒有切割(Cut)推理圖模式(即切割規(guī)則)出現(xiàn)的LK 或LJ推導(dǎo)[4]P298。它是矢列演算的核心結(jié)論，顯示了建立矢列演算系統(tǒng)的重要性，對包括一致性等元理論成果具有深遠(yuǎn)的影響。因此，根岑給出了該定理的完整證明過程[5]P298-306。在LK 和LJ推導(dǎo)中，一方面，切割消去定理保證能夠根據(jù)子公式性質(zhì)(the subformula property)從根部(root)出發(fā)向上進(jìn)行證明搜索；另一方面，正如布洛斯(George Boolos)所言，應(yīng)用切割規(guī)則會極大地減少推導(dǎo)的長度[6]。

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

二、G3cp系統(tǒng)

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

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

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

邏輯公理：

P,Γ?Δ,P

邏輯規(guī)則：

定義1*本文中加粗的“定義”、“定理”和“推論”采用順序表示法，特此說明。：一個公式A的權(quán)重(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系統(tǒng)中，一個推導(dǎo)或者是一個邏輯公理，或者是L⊥的一個實(shí)例(結(jié)論)，或者是一個邏輯規(guī)則應(yīng)用到包含它的前提的推導(dǎo)；一個推導(dǎo)的高度是連續(xù)應(yīng)用邏輯規(guī)則的最大數(shù)目，其中，邏輯公理和L⊥的推導(dǎo)高度為0。

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

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

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

因此，需要證明該規(guī)則在G3cp系統(tǒng)中是可容許的；而且，我們發(fā)現(xiàn)內(nèi)格里和柏拉圖關(guān)于切割規(guī)則的可容許性定理證明存在以下四個問題：

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

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

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

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

(三)收縮規(guī)則指代含混

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

在G3cp中，導(dǎo)出的收縮規(guī)則為：

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

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

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

四、切割規(guī)則的可容許性定理的證明

定理3：切割規(guī)則，

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

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

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

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

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

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

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

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

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

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

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

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

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

當(dāng)Γ=A∧B,?！鍟r，推導(dǎo)

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

轉(zhuǎn)換為推導(dǎo)

1.發(fā)揮資源優(yōu)勢，做強(qiáng)冰雪旅游產(chǎn)業(yè)。冰雪旅游業(yè)是冰雪產(chǎn)業(yè)的主體，發(fā)展冰雪產(chǎn)業(yè)，首先要做強(qiáng)冰雪旅游業(yè)。吉林省應(yīng)以冰雪資源優(yōu)勢為基礎(chǔ)，以長吉都市、長白山、查干湖地區(qū)為中心，結(jié)合地域特色，實(shí)現(xiàn)錯位有序發(fā)展，建成“一山、兩城、三區(qū)”的冰雪旅游產(chǎn)業(yè)空間發(fā)展布局，構(gòu)建知名冰雪產(chǎn)業(yè)品牌。

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

當(dāng)Γ=A∨B,?！鍟r，推導(dǎo)

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

轉(zhuǎn)換為推導(dǎo)

當(dāng)Γ=A?B,?！鍟r，推導(dǎo)

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

轉(zhuǎn)換為推導(dǎo)

當(dāng)Δ=Δ″,A∧B時，推導(dǎo)

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

轉(zhuǎn)換為推導(dǎo)

當(dāng)Δ=Δ″,A∨B時，推導(dǎo)

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

轉(zhuǎn)換為推導(dǎo)

當(dāng)Δ=Δ″,A?B時，推導(dǎo)

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

轉(zhuǎn)換為推導(dǎo)

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

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

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

當(dāng)Γ=A∧B,?！鍟r，推導(dǎo)

A,B,?！?Δ,DL∧

轉(zhuǎn)換為推導(dǎo)

當(dāng)Γ=A∨B,?！鍟r，推導(dǎo)

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

轉(zhuǎn)換為推導(dǎo)

當(dāng)Γ=A?B,?！鍟r，推導(dǎo)

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

轉(zhuǎn)換為推導(dǎo)

當(dāng)Δ=Δ″,A∧B時，推導(dǎo)

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

轉(zhuǎn)換為推導(dǎo)

當(dāng)Δ=Δ″,A∨B時，推導(dǎo)

Γ?Δ″,A,B,DR∨

轉(zhuǎn)換為推導(dǎo)

當(dāng)Δ=Δ″,A?B時，推導(dǎo)

A,Γ?Δ″,B,DR?

轉(zhuǎn)換為推導(dǎo)

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

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

當(dāng)?！?A∨B,?！鍟r，推導(dǎo)

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

轉(zhuǎn)換為推導(dǎo)

當(dāng)?！?A∨B,Γ″時，推導(dǎo)

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

轉(zhuǎn)換為推導(dǎo)

當(dāng)?！?A?B,?！鍟r，推導(dǎo)

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

轉(zhuǎn)換為推導(dǎo)

當(dāng)Δ′=Δ″,A∧B時，推導(dǎo)

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

轉(zhuǎn)換為推導(dǎo)

當(dāng)Δ′=Δ″,A∨B時，推導(dǎo)

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

轉(zhuǎn)換為推導(dǎo)

當(dāng)Δ′=Δ″,A?B時，推導(dǎo)

D,A,Γ′?Δ″,BR?

轉(zhuǎn)換為推導(dǎo)

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

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

當(dāng)D=A∧B時，推導(dǎo)

轉(zhuǎn)換為推導(dǎo)

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

當(dāng)D=A∨B時，推導(dǎo)

轉(zhuǎn)換為推導(dǎo)

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

當(dāng)D=A?B時，推導(dǎo)

轉(zhuǎn)換為推導(dǎo)

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

五、G3cp系統(tǒng)的推論

推論4：在G3cp中，關(guān)于矢列式在Γ?Δ推導(dǎo)中的所有公式是Γ和Δ的子公式[21]P57。因為G3cp沒有結(jié)構(gòu)規(guī)則，通過觀察它的邏輯公理和邏輯規(guī)則，可以立即得出這一推論。

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

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

六、結(jié)語

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

[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.

責(zé)任編輯：陳 剛

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

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