根岑邏輯演繹思想的
主要特徵和哲學影響探析
郭美雲
作者簡介：郭美雲， 西南大學 邏輯與智慧研究中心， 重慶 400715 郭美雲(1976- )， 江西吉安人， 哲學博士， 西南大學邏輯與智慧研究中心教授， 主要研究方向：現代邏輯理論及其應用、邏輯哲學和博弈邏輯。
人大複印：《邏輯》2016 年 04 期
原發期刊：《自然辯證法研究》2016 年第 20168 期 第 84-89 頁
摘要：論文在梳理根岑如何從邏輯公理化思想出發發展出自然演繹和矢列演算思想的基礎上， 總結出根岑邏輯演繹思想的主要特徵。 根岑對聯接詞引入和消去規則各自角色的理解及其採取的樹形證明方式引導他發現並證明了切割消去定理。
一、引言
根岑(G.Gentzen， 1909-1945)和雅斯科夫斯基(S.Jaskowski， 1906-1965)被認為是自然演繹(Natural Deduction)的獨立發現者和創立者。 盧凱西維其(Jan Lukasiewicz)在1926年的一個討論班上， 提出數學證明並不像當時的邏輯公理化思想那樣， 而是允許隨時引入假設。 雅斯科夫斯基後來用兩種表示方法來實現盧凱西維其的這一思想。 一種是通過框型圖對各級子證明進行標識， 另一種是對組成證明的公式序列進行記帳式的注釋(bookkeeping annotation)[1]232-258， 從而追蹤被引入的假設及其邏輯後承。 同時， 根岑在他的博士論文基礎上發表了題為《邏輯演繹研究》的論文[2]68-131， 獨立提出了自然演繹思想。
根岑把希爾伯特提出的算術一致性問題作為自己的目標， 自然演繹和矢列演算都只是解決這個問題過程中發展出來的工具和手段即副產品。 根岑用下面一段話表明了自己的動機和出發點：
我的出發點是這樣的：弗雷格、羅素和希爾伯特等人提出的關於邏輯推演的形式化系統儘管有相當多的形式化優勢， 但和實際數學證明中的推演形式相距甚遠。
這段話後來成為人們探索根岑邏輯演繹思想來源的主要源頭。 但在2005年一篇根岑的手稿重新被發現[3]240-244， 為人們追蹤和把握根岑邏輯演繹思想的發展脈絡提供了新的材料。
二、從公理化系統到自然演繹
受當時數學邏輯主義思潮的影響， 根岑把數學中普遍存在的各種推理形式看作是邏輯的研究物件。
下面的研究是關於謂詞邏輯的範圍。 它由數學中所有部分一直使用的各種類型的推理所組成。 需要補充的是被認為是數學特定分支中獨特的公理和各種形式的推理， 例如在初等數論中關於自然數的加法、乘法、冪運算的公理，
哥德爾在1931年的不完全性定理表明， 算術一致性的證明不能在系統本身中得到證明。 Von Plato通過研究根岑的手稿和根岑與Heyting和Kneser等人的信件發現， 早1932年初根岑就把算術的一致性證明作為自己的研究計畫， 1932年9月就已經逐步明確了自然演繹的基本規則[3]314-315。 因此， 根岑的主要興趣僅僅在於如何通過證明的方式建立數學證明， 從而決定他一開始就與關注真的模型論方法分道揚鑣。 正是從證明算術一致性的目標出發， 根岑需要先理清謂詞邏輯的證明系統， 再在此基礎上增加算術公理和規則， 從而逐步用證明論的手段證明算術的一致性。
邏輯公理化系統的思想源遠流長，
上述1、2、3條公理分別對應到矢列演算中弱化規則、收縮規則和切割規則三條結構規則， 4和5條公理分別對應自然演繹的合取引入和消去規則，公理6、7分別對應到析取引入和消去規則，公理8、9、10則是關於否定的規則。公理和規則的轉換在有了演繹定理之後，它們相互之間的轉換變得非常簡單。根岑抓住數學實際推理中隨時可以引入假設這一根本特點，從而提出了自然演繹。
如果將┒A定義為(A→⊥)，那麼(7)否定引入規則和(8)否定消去規則的第一條都是不必要的，因為它們分別是蘊涵引入規則和蘊涵消去規則的特例。
增加以下任何一個規則可以得到經典命題邏輯的自然演繹系統。
根岑的自然演繹系統有以下三個主要特徵：
在進行自然演繹的過程中，假設總是要根據某一條有假設規則而被消除。因此，依賴假設的轄域是其自然演繹思想中的一個核心概念。
每條基本規則中有且僅包含有一個邏輯常項，即每個邏輯常項的規則都是各自獨立和分離的，這條性質通常被稱為分離性(Separation)。
邏輯聯接詞的規則通常都是成對出現的，一條是引入規則，一條是消去規則。引入規則允許推演得到一個主聯接詞為該邏輯常項的公式。而消去規則使得我們可以從主聯接詞為該邏輯常項的公式得到其子公式。
根岑用方括號標明假設，並採取了樹形的證明書寫方式。樹形證明方式使得我們能夠精確地討論證明中的每個公式及其出現，從而更為細緻地研究其性質。Von Plato認為這種樹形結構的最大優勢在於我們能夠對應用規則的順序進行交換從而對演繹進行重新排列和組合[3]314。正是這種方法論上的優勢使得根岑能夠更加深入地研究自然演繹的性質，進而提出矢列演算，從而取得了具有里程碑意義的證明論結果——切割消去定理。
三、從自然演繹到矢列演算
根岑提出矢列演算的根本原因在於技術性需要：
關於自然演繹特定性質的更深入研究最後把我引到了一個非常具有普遍性的定理，後面我把它稱為Hauptsatz定理。……為了更方便地清楚表達和證明Hauptsatz定理，為了特別適合這一目的，我不得不提供(另外)一個邏輯演算[2]68。
根岑把矢列演算中的一個證明定義為從A├A這樣的基本矢列出發使用以上規則得到的一個公式樹。與自然演繹相比，矢列演算不僅關注論證的結論，還關注前提及整個過程，並且結論還不限於一個，是自然演繹的推廣。矢列演算系統的每個規則都可以看作如何從一個或兩個演繹得到另一個演繹的操作指南，即如何將一個或兩個證明(或者說論證)轉換為另一個證明。因此，矢列演算系統可以看作是自然演繹系統的元演算(Meta-calculi)[4]90。這些結構規則在自然演繹中是隱形的，我們往往是憑著直觀在使用。
上述規則除切割規則外，每條規則所用到的推演公式都是所得到的推演公式的子公式。根岑通過對推演中切割公式的複雜度和高度進行雙向歸納，成功地證明了任意一個推演都可以轉換為不需要切割規則的推演就切割消去定理，從而同時表明經典邏輯和直覺主義的矢列演算系統中的推演都具有子公式性質。因為任意一個公式的子公式顯然是有窮的，從而可以把這一定理應用到不可演繹性(Non-derivability)的證明以及不用歸納法對算術系統的一致性進行證明，還可以應用到電腦科學中的自動證明搜索。
四、根岑邏輯演繹思想的主要特徵
和雅思可夫斯基不同，根岑提出的兩個演算的一個主要特徵是包含命題聯接詞和量詞在內的大多邏輯常項(Logical Constants)都由一對規則組成。在自然演繹系統中，除否定聯接詞外，每個聯接詞都由引入規則和消去規則組成。根岑對引入規則和消去規則各自的角色有著他自己深刻而獨到的認識：
引入(規則)可以說是代表了所涉及(邏輯)符號的定義，而消去(規則)歸根結底僅僅是這些定義的後果。這一事實可以表述如下：在對一個公式的主聯接詞(Terminal Symbol)進行消去的時候，我們僅僅是在使用其引入這一符號時所規定的意義[2]80。
Prawitz把在使用一個聯接詞的引入規則之後再使用同一個聯接詞的消去規則稱作彎路(Detour)。根岑上述思想的一個直接後果就是，可以通過不斷歸約(Reduction)的方法將所有這樣的彎路全部消去，從而把所有自然演繹都轉換為一個具有相同結論但不含任何彎路的正規證明形式，一個具有這種正規形式的證明通常被稱作典範證明(Canonical Proof)。例如，在使用蘊涵引入規則之後再使用蘊涵消去規則的推演就可以轉換為一個正規形式。
在上例左圖中，[A]表示在蘊涵引入時所消去的假設，(A→B)被稱作大前提，而A被稱作小前提，因為左圖中已經存在一個關於小前提A的證明，因此用該證明替換假設A，就得到一個從A出發關於B的證明，從而得到一個不需要使用蘊涵引入規則和蘊涵消去規則的關於B的簡化證明。同理，關於合取和析取也可以作類似的處理。
在自然演繹中，上述歸約過程在碰到否定時會遇到問題。因為顯然關於否定的規則並不遵循一般意義上的引入和消去的成對關係。而在矢列演算系統中，除切割規則之外，包括否定聯接詞在內的所有其他規則都滿足子公式性質。矢列演算系統中切割消去定理的證明和自然演繹正規化定理的證明在效果上是一樣的。在矢列演算中，直覺主義邏輯成為經典邏輯的一個特例，即當上述規則中的結論只允許至多出現一個公式的時候，經典邏輯就變成了直覺主義邏輯。因此，根岑在矢列演算中同時證明了經典邏輯和直覺主義邏輯的切割消去定理。
五、根岑邏輯演繹思想的哲學影響
1.成為證明論語義學的思想源頭
證明論語義學(Proof-theoretical Semantics)這一術語正式出現在文獻中是Schroeder-Heister在1991年的一篇論文摘要裡提出來的，他指出，這一術語與Kutschera在1968年的一篇德文論文中曾使用過根岑語義學(Gentzen Semantics)一脈相承[5]1。因此，證明論語義學最終都被追溯到根岑。
證明論語義學是與邏輯上一直占統治地位的模型論語義學相對應而提出來的。模型論語義學本質上是指稱性的(Denotational)或表徵性的(Representational)，即意義是語言實體的指稱。根據模型論的觀點，一個語言運算式的意義在於它的指稱(Denotations)。一個語詞的意義是在語言-物件(Language-object Link)的二元關係中得以確立的。在模型論語義學中，從A語義推出B，被以下事實所證成(Justified)，即A的任何模型都是B的模型。這意味著我們自然而然地需要一個外部(External)語義學對證明的合法性做出說明。因此，模型論語義學需要一個外在的語義模型賦予語法物件以意義。
證明論語義學作為另一種語義學進路主要基於根岑邏輯演算中體現的以下兩個基本思想，一是邏輯聯接詞的意義能夠通過設立的一些推理模式和規則得到解釋。另一個思想是規則的可靠性能夠從規則的性質出發通過一些證明論論證演繹出來。希爾伯特式的形式主義綱領認為語形證明僅僅是公式的語法變形，其本身和意義無關。而證明論語義學(Proof-theoretical Semantics)則賦予證明本身以意義，認為證明或演繹本身就自動扮演著語義的角色。
模型論語義學又被稱作真值條件語義學(truth-condition Semantics)，證明論語義學的一個重要出發點在於對真這一語義概念的理解上。例如Goran Sundholm提出：命題A是真的當且僅當存在關於的A的一個真值製造者(Truth-maker)，更進一步地，命題A是真的當且僅當存在關於的A的一個證明(Proof)。Goran Sundholm還對證明作了一個更為寬泛的解釋，並且從詞源學的角度認為，證明不僅僅是指數學意義上的證明，還包括法律論證中的測試(test)[6]294-314。Schroeder-Heister則認為，證明不能簡單地理解為形式推演，而應把證明進一步推廣到我們用來表達論證和據此獲取知識的實體(Entities)[7]253。
證明論語義學建立在這樣一個基本假設的基礎之上，即我們賦予語言運算式，特別是邏輯常項的意義是根據證明而不是真值的。證明論語義學是關於證明的語義學(Semantics of Proofs)，證明論語義學認為，這些證明的語義恰恰可以根據這些證明本身得到說明。
當今證明論語義學的重要宣導者Schroeder-Heister認為，弗雷格當然知道蘊涵在演繹中的重要性，因此在他給出的公理化系統中把蘊涵作為初始聯接詞。但在弗雷格的公理化系統中，物件語言中的→這一符號有兩個作用，一個是作為命題聯接詞表達了一個條件命題A→B。另一個作用是在公理化系統中表達A推出B[7]257。這在公理化系統的演繹定理這一元定理當中表現得最為明顯。因為已經有蘊涵聯接詞在手上，因此無需考慮假設性證明。Schroeder-Heister認為正是弗雷格關於蘊涵的這種單層次概念(single-layer concept of implication)使得弗雷格認為一個蘊涵式的證成(Justification)不是根據蘊涵的引入規則，而必需借助於公理的有效性和規則的保有效性這種可靠性定理的元定理證明來證成[8]257。
從更廣的範圍來看，證明論語義學同布蘭頓(Brandom)自2000年以來提出的推理主義(Inferentialism)哲學思潮一脈相承，推理主義反對模型論語義學的哲學基礎——表徵主義(Representionalism)，認為是推理和推理規則而不是表徵或指稱建立起了語言運算式的意義。Tennant就認為，“一個推理主義的意義理論堅持一個邏輯運算元的意義是能夠(在自然演繹這樣的系統中)被適當的推理規則所捕獲的”[8]1055-1078。這和證明論語義學主張推理活動是在證明自身中所彰顯出來的立場是一致的。德國圖賓根大學分別於1999年和2013年一共組織了兩屆題為“證明論語義學”的國際會議。目前證明論語義學已取得了一些進展，正逐步受到重視和認可。
2.對意義理論的影響
受根岑思想的啟發，Prior發明了一個新的命題聯接詞，他將其命名為tonk，其引入規則是：從A可以得到A tonk B；消去規則為：從A tonk B可以得到B[9]38-39。這一對規則分別從使用的角度規定了tonk的用法，但通過傳遞性不難發現，從這兩條規則允許我們從任意命題A得到任意命題B，而這顯然是荒謬的。貝爾納普認為tonk的問題在於它的擴充是不保守的(Non-conseruative)。因為它的有效性只是在包含Tonk的語言中得到了驗證，而不能在沒有包含Tonk的語言中得到驗證。受Prior的啟發，貝爾納普還提出了一些諸如Plonk和Plink等一些更為古怪的聯接詞[10]130-134。
達米特從語言學實踐和意義理論這一更為廣泛的角度看待自然演繹中引入規則和消去規則的相互關係。傳統的意義理論把一個句子的真之條件當作一個句子的意義。而達米特認為這對一個足夠的意義理論是不足夠的。達米特堅持並力圖貫徹“語言的意義在於如何被使用”這一口號，為此他把任何一個諸如句子、項、謂詞和聯接詞等這樣一些有意義的語言單位的使用區分為最為基本的兩個方面，一方面是近似於使用這些運算式的條件(Conditions)或根據(Grounds)，另一方面是使用它們的後果(Consequences)[11]55。在斷言中，一個運算式的根據包括那些能夠推出斷言句(Asserted Sentence)的那些主張，還包括說話者觀察到的事態(state of affairs)。而一個運算式的後果則可以包括說話者和聽眾的相應行動。他認為單詞僅僅在一個句子的語境中才有意義，並且主張一個運算式的後果可以歸約它們其中的句子當中。在這兩點上，達米特和弗雷格原子主義的思想是一致的。達米特認為，在語言學習中掌握一個運算式這兩個方面的使用正是它的意義之所在。
達米特還進一步將貝爾納普擴張保守性的要求運用到他自己提出來的這兩個方面的關係上，要求條件與後果的和諧。他認為，正是和諧性的要求使得我們可以批評語言實踐過程中遇到的問題。
一個簡單地情形是那些輕蔑性運算式，例如“Boche”(德國佬)。將這個詞項應用到某人的條件是他具有德國國籍；使用它的後果是他殘暴且對其他歐洲人很殘忍。這兩個方面聯繫如此之緊密以至於這就組成了這個詞的本來意義。我們應該正視這一點，在沒有改變它意義的前提下，任何一個方面都割離不了。拒斥這個詞的人這樣做只是因為他不允許將這個詞的使用條件轉換到使用後果上來。將“Boche”這個詞加入到本來先前沒有它的語言之中將會產生一個不保守擴充，即在該擴充中一些沒有包含該詞項的一些陳述能夠從一些也不包含該詞項的陳述中推斷出來，而它們先前是不可推斷出來的[12]454-455……
達米特還從語言學實踐和意義理論這一更為廣泛的角度看待自然演繹中引入規則和消去規則的相互關係。達米特在《形而上學的邏輯基礎》中對證明論語義學的哲學基礎做了不少工作並產生了很大的影響。
正規化定理的一個重要推論是直覺主義邏輯中每個封閉的推演都能夠被轉化為一個最後一步是引入規則的推演。達米特在《形而上學的邏輯基礎》一書中把它作為基本假設，並將這一證明論技術結果作為哲學說明的一個典型例子[13]。
從證明的角度出發解讀自然演繹中的規則，使得自然演繹和數學中的直覺主義思潮即構造主義思想有著天然的內在聯繫，從而使得自然演繹邏輯天然地偏向於直覺主義邏輯。達米特更進一步認為，經典邏輯的自然演繹系統的引入規則和消去規則是不協調的，而直接主義邏輯的自然演繹系統的引入和消去規則是協調的，並且排中律不是自我辯護的(Self-justfying)，進而把是否接受排中律作為實在論的劃界標準[14]，可以說，正是邏輯的直覺主義立場把他引向了哲學上的反實在論立場。因為實在論一般認為，所有句子的真假是獨立於我們而存在的一個客觀實在，與我們認識它們的手段無關。
參考文獻：
[1]S.Jaskowski.On the Rules of Suppositions in Formal Logic[J].Studia Logica,1934,1.Reprinted in S.McCall,Polish Logic 1920-1939,Oxford Univ.Press,1967:232-258.
[2]G.Gentzen.Untersuchungen über das logische Schliessen,Mathematische Zeitschrift.1934.Translated as“Investigations Into Logical Deduction” and printed in M.Szabo,The Collected Papers of Gerhard Gentzen[M].Amsterdam:North-Holland,1969.
[3]J.Von Plato.Gentzen’s Proof of Normalization for Natural Deduction[J].The Bulletin of Symbolic Logic,2008,14:240-244.
[4]D.Prawitz.Natural Deduction:A Proof-Theoretic Study[M].New-York:Dover Publications Inc.,1965.
[5]R.Kahle,P.Schroeder-Heister.Introduction:Proof-theoretic Semantics[C]//T.Piecha,P.Schroeder-Heister.Advances in Proof-theoretic Semantics.Springer,2015.
[6]G.Sundholm.Proof-theoretic Semantics and Fregen Identity Criteria for Propositions[J].The Monist,1994,77(3)Vol.77:294-314.
[7]P.Schroeder-Heister,Open problems in Proof-theoretic Semantics[C]//T.Piecha,P.Schroeder-Heister.Advances in Proof-theoretic Semantics.Springer,2015.
[8]N.Tennant.Existence and Identity in Free Logic:A Problem for Inferentialsim?[J].Mind,2007.116:1055-1078.
[9]A.Prior.The Runabout Inference-ticket[J].Analysis,1960,21(2):38-39.
[10]N.Belnap.Tonk,Plonk and Plink[J].Analysis,1962,22:130-134.
[11]M.Kremer.Logic and Meaning:the Philosophical Significance of Sequent Calculus[J].Mind,1988,(385):50-72.
[12]M.Dummett.Frege:Philosophy of Language[M].New York:Harper and Row,1973.
[13]P.Schroeder-Heister.Proof-Theoretical Semantics[EB/OL]2012,http://plato.stanford.edu/entries/proof-theoretical-semantics.
4和5條公理分別對應自然演繹的合取引入和消去規則，公理6、7分別對應到析取引入和消去規則，公理8、9、10則是關於否定的規則。公理和規則的轉換在有了演繹定理之後，它們相互之間的轉換變得非常簡單。根岑抓住數學實際推理中隨時可以引入假設這一根本特點，從而提出了自然演繹。如果將┒A定義為(A→⊥)，那麼(7)否定引入規則和(8)否定消去規則的第一條都是不必要的，因為它們分別是蘊涵引入規則和蘊涵消去規則的特例。
增加以下任何一個規則可以得到經典命題邏輯的自然演繹系統。
根岑的自然演繹系統有以下三個主要特徵：
在進行自然演繹的過程中，假設總是要根據某一條有假設規則而被消除。因此，依賴假設的轄域是其自然演繹思想中的一個核心概念。
每條基本規則中有且僅包含有一個邏輯常項，即每個邏輯常項的規則都是各自獨立和分離的，這條性質通常被稱為分離性(Separation)。
邏輯聯接詞的規則通常都是成對出現的，一條是引入規則，一條是消去規則。引入規則允許推演得到一個主聯接詞為該邏輯常項的公式。而消去規則使得我們可以從主聯接詞為該邏輯常項的公式得到其子公式。
根岑用方括號標明假設，並採取了樹形的證明書寫方式。樹形證明方式使得我們能夠精確地討論證明中的每個公式及其出現，從而更為細緻地研究其性質。Von Plato認為這種樹形結構的最大優勢在於我們能夠對應用規則的順序進行交換從而對演繹進行重新排列和組合[3]314。正是這種方法論上的優勢使得根岑能夠更加深入地研究自然演繹的性質，進而提出矢列演算，從而取得了具有里程碑意義的證明論結果——切割消去定理。
三、從自然演繹到矢列演算
根岑提出矢列演算的根本原因在於技術性需要：
關於自然演繹特定性質的更深入研究最後把我引到了一個非常具有普遍性的定理，後面我把它稱為Hauptsatz定理。……為了更方便地清楚表達和證明Hauptsatz定理，為了特別適合這一目的，我不得不提供(另外)一個邏輯演算[2]68。
根岑把矢列演算中的一個證明定義為從A├A這樣的基本矢列出發使用以上規則得到的一個公式樹。與自然演繹相比，矢列演算不僅關注論證的結論，還關注前提及整個過程，並且結論還不限於一個，是自然演繹的推廣。矢列演算系統的每個規則都可以看作如何從一個或兩個演繹得到另一個演繹的操作指南，即如何將一個或兩個證明(或者說論證)轉換為另一個證明。因此，矢列演算系統可以看作是自然演繹系統的元演算(Meta-calculi)[4]90。這些結構規則在自然演繹中是隱形的，我們往往是憑著直觀在使用。
上述規則除切割規則外，每條規則所用到的推演公式都是所得到的推演公式的子公式。根岑通過對推演中切割公式的複雜度和高度進行雙向歸納，成功地證明了任意一個推演都可以轉換為不需要切割規則的推演就切割消去定理，從而同時表明經典邏輯和直覺主義的矢列演算系統中的推演都具有子公式性質。因為任意一個公式的子公式顯然是有窮的，從而可以把這一定理應用到不可演繹性(Non-derivability)的證明以及不用歸納法對算術系統的一致性進行證明，還可以應用到電腦科學中的自動證明搜索。
四、根岑邏輯演繹思想的主要特徵
和雅思可夫斯基不同，根岑提出的兩個演算的一個主要特徵是包含命題聯接詞和量詞在內的大多邏輯常項(Logical Constants)都由一對規則組成。在自然演繹系統中，除否定聯接詞外，每個聯接詞都由引入規則和消去規則組成。根岑對引入規則和消去規則各自的角色有著他自己深刻而獨到的認識：
引入(規則)可以說是代表了所涉及(邏輯)符號的定義，而消去(規則)歸根結底僅僅是這些定義的後果。這一事實可以表述如下：在對一個公式的主聯接詞(Terminal Symbol)進行消去的時候，我們僅僅是在使用其引入這一符號時所規定的意義[2]80。
Prawitz把在使用一個聯接詞的引入規則之後再使用同一個聯接詞的消去規則稱作彎路(Detour)。根岑上述思想的一個直接後果就是，可以通過不斷歸約(Reduction)的方法將所有這樣的彎路全部消去，從而把所有自然演繹都轉換為一個具有相同結論但不含任何彎路的正規證明形式，一個具有這種正規形式的證明通常被稱作典範證明(Canonical Proof)。例如，在使用蘊涵引入規則之後再使用蘊涵消去規則的推演就可以轉換為一個正規形式。
在上例左圖中，[A]表示在蘊涵引入時所消去的假設，(A→B)被稱作大前提，而A被稱作小前提，因為左圖中已經存在一個關於小前提A的證明，因此用該證明替換假設A，就得到一個從A出發關於B的證明，從而得到一個不需要使用蘊涵引入規則和蘊涵消去規則的關於B的簡化證明。同理，關於合取和析取也可以作類似的處理。
在自然演繹中，上述歸約過程在碰到否定時會遇到問題。因為顯然關於否定的規則並不遵循一般意義上的引入和消去的成對關係。而在矢列演算系統中，除切割規則之外，包括否定聯接詞在內的所有其他規則都滿足子公式性質。矢列演算系統中切割消去定理的證明和自然演繹正規化定理的證明在效果上是一樣的。在矢列演算中，直覺主義邏輯成為經典邏輯的一個特例，即當上述規則中的結論只允許至多出現一個公式的時候，經典邏輯就變成了直覺主義邏輯。因此，根岑在矢列演算中同時證明了經典邏輯和直覺主義邏輯的切割消去定理。
五、根岑邏輯演繹思想的哲學影響
1.成為證明論語義學的思想源頭
證明論語義學(Proof-theoretical Semantics)這一術語正式出現在文獻中是Schroeder-Heister在1991年的一篇論文摘要裡提出來的，他指出，這一術語與Kutschera在1968年的一篇德文論文中曾使用過根岑語義學(Gentzen Semantics)一脈相承[5]1。因此，證明論語義學最終都被追溯到根岑。
證明論語義學是與邏輯上一直占統治地位的模型論語義學相對應而提出來的。模型論語義學本質上是指稱性的(Denotational)或表徵性的(Representational)，即意義是語言實體的指稱。根據模型論的觀點，一個語言運算式的意義在於它的指稱(Denotations)。一個語詞的意義是在語言-物件(Language-object Link)的二元關係中得以確立的。在模型論語義學中，從A語義推出B，被以下事實所證成(Justified)，即A的任何模型都是B的模型。這意味著我們自然而然地需要一個外部(External)語義學對證明的合法性做出說明。因此，模型論語義學需要一個外在的語義模型賦予語法物件以意義。
證明論語義學作為另一種語義學進路主要基於根岑邏輯演算中體現的以下兩個基本思想，一是邏輯聯接詞的意義能夠通過設立的一些推理模式和規則得到解釋。另一個思想是規則的可靠性能夠從規則的性質出發通過一些證明論論證演繹出來。希爾伯特式的形式主義綱領認為語形證明僅僅是公式的語法變形，其本身和意義無關。而證明論語義學(Proof-theoretical Semantics)則賦予證明本身以意義，認為證明或演繹本身就自動扮演著語義的角色。
模型論語義學又被稱作真值條件語義學(truth-condition Semantics)，證明論語義學的一個重要出發點在於對真這一語義概念的理解上。例如Goran Sundholm提出：命題A是真的當且僅當存在關於的A的一個真值製造者(Truth-maker)，更進一步地，命題A是真的當且僅當存在關於的A的一個證明(Proof)。Goran Sundholm還對證明作了一個更為寬泛的解釋，並且從詞源學的角度認為，證明不僅僅是指數學意義上的證明，還包括法律論證中的測試(test)[6]294-314。Schroeder-Heister則認為，證明不能簡單地理解為形式推演，而應把證明進一步推廣到我們用來表達論證和據此獲取知識的實體(Entities)[7]253。
證明論語義學建立在這樣一個基本假設的基礎之上，即我們賦予語言運算式，特別是邏輯常項的意義是根據證明而不是真值的。證明論語義學是關於證明的語義學(Semantics of Proofs)，證明論語義學認為，這些證明的語義恰恰可以根據這些證明本身得到說明。
當今證明論語義學的重要宣導者Schroeder-Heister認為，弗雷格當然知道蘊涵在演繹中的重要性，因此在他給出的公理化系統中把蘊涵作為初始聯接詞。但在弗雷格的公理化系統中，物件語言中的→這一符號有兩個作用，一個是作為命題聯接詞表達了一個條件命題A→B。另一個作用是在公理化系統中表達A推出B[7]257。這在公理化系統的演繹定理這一元定理當中表現得最為明顯。因為已經有蘊涵聯接詞在手上，因此無需考慮假設性證明。Schroeder-Heister認為正是弗雷格關於蘊涵的這種單層次概念(single-layer concept of implication)使得弗雷格認為一個蘊涵式的證成(Justification)不是根據蘊涵的引入規則，而必需借助於公理的有效性和規則的保有效性這種可靠性定理的元定理證明來證成[8]257。
從更廣的範圍來看，證明論語義學同布蘭頓(Brandom)自2000年以來提出的推理主義(Inferentialism)哲學思潮一脈相承，推理主義反對模型論語義學的哲學基礎——表徵主義(Representionalism)，認為是推理和推理規則而不是表徵或指稱建立起了語言運算式的意義。Tennant就認為，“一個推理主義的意義理論堅持一個邏輯運算元的意義是能夠(在自然演繹這樣的系統中)被適當的推理規則所捕獲的”[8]1055-1078。這和證明論語義學主張推理活動是在證明自身中所彰顯出來的立場是一致的。德國圖賓根大學分別於1999年和2013年一共組織了兩屆題為“證明論語義學”的國際會議。目前證明論語義學已取得了一些進展，正逐步受到重視和認可。
2.對意義理論的影響
受根岑思想的啟發，Prior發明了一個新的命題聯接詞，他將其命名為tonk，其引入規則是：從A可以得到A tonk B；消去規則為：從A tonk B可以得到B[9]38-39。這一對規則分別從使用的角度規定了tonk的用法，但通過傳遞性不難發現，從這兩條規則允許我們從任意命題A得到任意命題B，而這顯然是荒謬的。貝爾納普認為tonk的問題在於它的擴充是不保守的(Non-conseruative)。因為它的有效性只是在包含Tonk的語言中得到了驗證，而不能在沒有包含Tonk的語言中得到驗證。受Prior的啟發，貝爾納普還提出了一些諸如Plonk和Plink等一些更為古怪的聯接詞[10]130-134。
達米特從語言學實踐和意義理論這一更為廣泛的角度看待自然演繹中引入規則和消去規則的相互關係。傳統的意義理論把一個句子的真之條件當作一個句子的意義。而達米特認為這對一個足夠的意義理論是不足夠的。達米特堅持並力圖貫徹“語言的意義在於如何被使用”這一口號，為此他把任何一個諸如句子、項、謂詞和聯接詞等這樣一些有意義的語言單位的使用區分為最為基本的兩個方面，一方面是近似於使用這些運算式的條件(Conditions)或根據(Grounds)，另一方面是使用它們的後果(Consequences)[11]55。在斷言中，一個運算式的根據包括那些能夠推出斷言句(Asserted Sentence)的那些主張，還包括說話者觀察到的事態(state of affairs)。而一個運算式的後果則可以包括說話者和聽眾的相應行動。他認為單詞僅僅在一個句子的語境中才有意義，並且主張一個運算式的後果可以歸約它們其中的句子當中。在這兩點上，達米特和弗雷格原子主義的思想是一致的。達米特認為，在語言學習中掌握一個運算式這兩個方面的使用正是它的意義之所在。
達米特還進一步將貝爾納普擴張保守性的要求運用到他自己提出來的這兩個方面的關係上，要求條件與後果的和諧。他認為，正是和諧性的要求使得我們可以批評語言實踐過程中遇到的問題。
一個簡單地情形是那些輕蔑性運算式，例如“Boche”(德國佬)。將這個詞項應用到某人的條件是他具有德國國籍；使用它的後果是他殘暴且對其他歐洲人很殘忍。這兩個方面聯繫如此之緊密以至於這就組成了這個詞的本來意義。我們應該正視這一點，在沒有改變它意義的前提下，任何一個方面都割離不了。拒斥這個詞的人這樣做只是因為他不允許將這個詞的使用條件轉換到使用後果上來。將“Boche”這個詞加入到本來先前沒有它的語言之中將會產生一個不保守擴充，即在該擴充中一些沒有包含該詞項的一些陳述能夠從一些也不包含該詞項的陳述中推斷出來，而它們先前是不可推斷出來的[12]454-455……
達米特還從語言學實踐和意義理論這一更為廣泛的角度看待自然演繹中引入規則和消去規則的相互關係。達米特在《形而上學的邏輯基礎》中對證明論語義學的哲學基礎做了不少工作並產生了很大的影響。
正規化定理的一個重要推論是直覺主義邏輯中每個封閉的推演都能夠被轉化為一個最後一步是引入規則的推演。達米特在《形而上學的邏輯基礎》一書中把它作為基本假設，並將這一證明論技術結果作為哲學說明的一個典型例子[13]。
從證明的角度出發解讀自然演繹中的規則，使得自然演繹和數學中的直覺主義思潮即構造主義思想有著天然的內在聯繫，從而使得自然演繹邏輯天然地偏向於直覺主義邏輯。達米特更進一步認為，經典邏輯的自然演繹系統的引入規則和消去規則是不協調的，而直接主義邏輯的自然演繹系統的引入和消去規則是協調的，並且排中律不是自我辯護的(Self-justfying)，進而把是否接受排中律作為實在論的劃界標準[14]，可以說，正是邏輯的直覺主義立場把他引向了哲學上的反實在論立場。因為實在論一般認為，所有句子的真假是獨立於我們而存在的一個客觀實在，與我們認識它們的手段無關。
參考文獻：
[1]S.Jaskowski.On the Rules of Suppositions in Formal Logic[J].Studia Logica,1934,1.Reprinted in S.McCall,Polish Logic 1920-1939,Oxford Univ.Press,1967:232-258.
[2]G.Gentzen.Untersuchungen über das logische Schliessen,Mathematische Zeitschrift.1934.Translated as“Investigations Into Logical Deduction” and printed in M.Szabo,The Collected Papers of Gerhard Gentzen[M].Amsterdam:North-Holland,1969.
[3]J.Von Plato.Gentzen’s Proof of Normalization for Natural Deduction[J].The Bulletin of Symbolic Logic,2008,14:240-244.
[4]D.Prawitz.Natural Deduction:A Proof-Theoretic Study[M].New-York:Dover Publications Inc.,1965.
[5]R.Kahle,P.Schroeder-Heister.Introduction:Proof-theoretic Semantics[C]//T.Piecha,P.Schroeder-Heister.Advances in Proof-theoretic Semantics.Springer,2015.
[6]G.Sundholm.Proof-theoretic Semantics and Fregen Identity Criteria for Propositions[J].The Monist,1994,77(3)Vol.77:294-314.
[7]P.Schroeder-Heister,Open problems in Proof-theoretic Semantics[C]//T.Piecha,P.Schroeder-Heister.Advances in Proof-theoretic Semantics.Springer,2015.
[8]N.Tennant.Existence and Identity in Free Logic:A Problem for Inferentialsim?[J].Mind,2007.116:1055-1078.
[9]A.Prior.The Runabout Inference-ticket[J].Analysis,1960,21(2):38-39.
[10]N.Belnap.Tonk,Plonk and Plink[J].Analysis,1962,22:130-134.
[11]M.Kremer.Logic and Meaning:the Philosophical Significance of Sequent Calculus[J].Mind,1988,(385):50-72.
[12]M.Dummett.Frege:Philosophy of Language[M].New York:Harper and Row,1973.
[13]P.Schroeder-Heister.Proof-Theoretical Semantics[EB/OL]2012,http://plato.stanford.edu/entries/proof-theoretical-semantics.