甘岑后繼式演算系統(tǒng)與其自然演繹系統(tǒng)的比較

董文媛

?

甘岑后繼式演算系統(tǒng)與其自然演繹系統(tǒng)的比較

董文媛

（山西農(nóng)業(yè)大學(xué)信息學(xué)院創(chuàng)意寫作中心，山西 太谷030800）

《邏輯演繹研究》“（Untersuchungen über das Logische Schliessen”）是甘岑提交哥廷根大學(xué)的就職論文，文中甘岑提出了兩種邏輯演算系統(tǒng)，即“自然演繹”和“后繼式演算”系統(tǒng)。從自然演繹開始甘岑嘗試構(gòu)造一個(gè)接近數(shù)學(xué)實(shí)際推理的邏輯演算，而后針對自然演繹系統(tǒng)的不足進(jìn)行了轉(zhuǎn)化和改進(jìn)，構(gòu)造了后繼式演算系統(tǒng)，并證明了該邏輯演算系統(tǒng)的合理性。甘岑的邏輯演繹思想在邏輯史上具有十分重要的地位，對現(xiàn)代邏輯和證明論的發(fā)展具有深遠(yuǎn)的影響。

自然演繹；后繼式演算；邏輯演算系統(tǒng)

1　甘岑后繼式演算系統(tǒng)

1.1從“自然演繹”到“后繼式演算”

繼希爾伯特和阿克曼的《數(shù)理邏輯基礎(chǔ)》之后，甘岑（Gerhard Gentzen 1909-1945）于1934-1935年分兩部分發(fā)表的論文《邏輯演繹研究》（“Untersuchungen über das Logische Schliessen”英譯為“Investigations into logical deduction”）中提出了“自然演繹”（Natural deduction）的概念。哥德爾在不完全定理證明之后，進(jìn)一步提出了數(shù)論一致性的不可證問題，甘岑則以構(gòu)造數(shù)論的一致性證明為目標(biāo)，將邏輯演繹的形式化作為出發(fā)點(diǎn)進(jìn)行嘗試。他認(rèn)為弗雷格、羅素和希爾伯特的形式系統(tǒng)遠(yuǎn)離了數(shù)學(xué)證明中實(shí)際使用的演繹形式，因此為了使形式證明盡可能地接近自然的、實(shí)際的推理，使結(jié)論獨(dú)立于假設(shè)成為“純邏輯”的證明，并且達(dá)到可觀的形式上的優(yōu)越性，構(gòu)造了自然演繹系統(tǒng)。［1］288自然演繹是一種證明演算，在這種邏輯演算中，不同于公理系統(tǒng)演算包含公理和推理規(guī)則，自然演繹系統(tǒng)是只包含推理規(guī)則，更加接近自然的實(shí)際推理。

1.2后繼式演算

基于自然演繹系統(tǒng)存在的不足，甘岑嘗試建立一個(gè)新的邏輯演算系統(tǒng)，在自然演繹系統(tǒng)的基礎(chǔ)上進(jìn)行完善，分別構(gòu)建完善了古典謂詞邏輯和直覺主義謂詞邏輯的演算系統(tǒng)，為“切割消除定理”和數(shù)論一致性提供了完整的證明。一方面這個(gè)系統(tǒng)要繼承自然演繹推理規(guī)則中“引入”和“消去”的邏輯符號規(guī)則系統(tǒng)，另一方面要改變自然演繹的形式，這個(gè)系統(tǒng)是“邏輯的”，即其中的推導(dǎo)不含有假設(shè)公式。這個(gè)新的系統(tǒng)甘岑稱之為后繼式演算（Sequent Calculus）系統(tǒng)，同樣甘岑分別構(gòu)建了直覺主義謂詞邏輯后繼式演算系統(tǒng)（簡稱為“LJ”）和古典謂詞邏輯后繼式演算系統(tǒng)（簡稱為“LK”）。

在自然演繹NJ系統(tǒng)基礎(chǔ)上，甘岑做了一些改動(dòng)來構(gòu)建LJ系統(tǒng)。首先用新公式（A1&...&Aμ）éB來替換依賴于假設(shè)A1，...，Aμ的D-公式（推導(dǎo)公式）B。［1］295將所有這種情況下的D-公式這樣替換，我們就得到了（A1&...&Aμ）éB這種自身有效的公式，它們的真不再以一些假設(shè)公式的真為條件。但是這樣在推理圖的下層公式中就引入了新的邏輯符號&和é，所有的推理圖在原有基礎(chǔ)上都必須增加&和é的推理圖，這便擾亂了引入和消去邏輯符號系統(tǒng)的特征。因此，甘岑引入了后繼式的概念。

一個(gè)后繼式是具有如下形式的表達(dá)式［1］290：

A1，...，Aμ—→B1，...，Bv

其中A1，...，Aμ和B1，...，Bv可以代表任何公式，符號“—→”像逗號，是輔助符號，不是邏輯符號。公式A1，...，Aμ形成該后繼式的前件（Antecedent），公式B1，...，Bv則形成該后繼式的后件（Succedent）。這兩種表達(dá)式都可以為空。

后繼式與下面這個(gè)公式在直觀上有相同的意義：

（A1&...&Aμ）é（B1∨...∨Bv）

如果前件為空，那么這個(gè)后繼式就歸約為公式B1∨...∨Bv；

如果后件為空，那么這個(gè)后繼式與公式?（A1&...&Aμ）或（A1&...&Aμ）éF的意思相同；

如果前后件兩個(gè)部分都為空，那么這個(gè)后繼式意思與F相同，即為假命題。

反之，每個(gè)公式都有一個(gè)相應(yīng)的等價(jià)后繼式，例如前件為空而后件恰由那個(gè)公式構(gòu)成的后繼式（公式A等價(jià)于后繼式—→A）。

組成一個(gè)后繼式的公式稱為S-公式（即后繼式公式）。這樣規(guī)定我們是想表明，我們不是在考慮公式本身，而是考慮它在后繼式中的出現(xiàn)（與D-公式類似）。比如我們說：“一個(gè)公式作為一個(gè)S-公式在一個(gè)后繼式中幾處出現(xiàn)”，這也可以表達(dá)如下：“幾個(gè)不同的S-公式（這僅僅意謂：該公式在該后繼式中有不同的出現(xiàn)）在形式上是相等的”。［1］290也就是說一個(gè)公式，在后繼式中不同的位置出現(xiàn)，雖然形式相同，但是我們把它的每次出現(xiàn)都看作一個(gè)不同的S-公式。關(guān)于推理圖和推導(dǎo)的定義，后繼式演算沿用了自然演繹推理圖和推導(dǎo)的定義，只不過在后繼式演算的推理圖由上層后繼式和下層后繼式構(gòu)成，后繼式演算的證明仍然是樹形的。那么由一個(gè)后繼式構(gòu)成的推導(dǎo)中，一個(gè)推導(dǎo)中出現(xiàn)的后繼式稱為D-后繼式（即推導(dǎo)后繼式），D-后繼式的S-公式稱為D-S-公式（即推導(dǎo)后繼式公式）。［1］291

構(gòu)建LJ系統(tǒng)時(shí)我們不使用公式（A1&...&Aμ）éB這種形式，而寫成后繼式的形式：A1，...，Aμ—→B，根據(jù)后繼式的定義得知，這個(gè)公式與它的后繼式形式在直觀意義上沒有區(qū)別，只是在形式結(jié)構(gòu)上有所差別。［1］291

甘岑進(jìn)一步構(gòu)造了一些新的推理圖，這些推理圖不能整合到引入和消去推理圖系統(tǒng)中，它們不需要參照邏輯符號，而是參照后繼式的結(jié)構(gòu)，將這些推理圖在系統(tǒng)中保留特殊的位置。甘岑將這些新加入的關(guān)于后繼式結(jié)構(gòu)的推理圖稱為“結(jié)構(gòu)推理圖”，而其余的參照邏輯符號的推理圖稱為“算子推理圖”。以上甘岑構(gòu)造謂詞邏輯后繼式演算系統(tǒng)的主要方法。

此外，甘岑還解決了在古典謂詞邏輯自然演繹系統(tǒng)中，排中律無法整合入引入和消去的系統(tǒng)中的問題。在后繼式演算系統(tǒng)中，甘岑則運(yùn)用限制后繼式形式結(jié)構(gòu)上的差別來區(qū)別LJ系統(tǒng)和LK系統(tǒng)，即LJ-系統(tǒng)中只允許后件是不能超過一個(gè)S-公式的后繼式，而在LK系統(tǒng)中允許后件帶有多個(gè)S-公式的后繼式進(jìn)入。表面看來，結(jié)構(gòu)上的限制沒有體現(xiàn)排中律的特殊地位，但實(shí)際上，甘岑巧妙的運(yùn)用這樣的方法，在直覺主義謂詞邏輯后繼式演算系統(tǒng)中排除了排中律，即排中律“A∨?A”，其后繼式“—→A∨?A”在LK系統(tǒng)中可證，在LJ系統(tǒng)中不可證。如此看來，根據(jù)后繼式的定義，這樣得到的古典謂詞邏輯后繼式演算系統(tǒng)更符合后繼式的對稱性，在形式上更加優(yōu)雅。

甘岑構(gòu)造的后繼式演算系統(tǒng)，在形式上很大程度是由要證明他所提出的“法則”即“切割消除定理”相關(guān)的考慮決定的，而子公式性質(zhì)（Subformula property）則是這一“法則”的推論。因此，在后繼式演算系統(tǒng)中我們可以完整的證明這個(gè)形式系統(tǒng)的合理性，彌補(bǔ)了自然演繹系統(tǒng)的不足。

2　后繼式演算系統(tǒng)與自然演繹系統(tǒng)的比較

2.1系 統(tǒng)構(gòu)造比較

首先，后繼式演算系統(tǒng)的構(gòu)造是在自然演繹基礎(chǔ)上的一個(gè)拓展。自然演繹推理圖中的基本單位為公式，在一個(gè)推導(dǎo)中，結(jié)論是由一個(gè)公式構(gòu)成，在后繼式演算系統(tǒng)中，甘岑將推導(dǎo)的結(jié)論擴(kuò)展為一個(gè)公式后繼式，引進(jìn)了后繼式的概念A(yù)1，...，Aμ—→B1，...，Bv。為了避免推理圖產(chǎn)生混亂，甘岑用“—→”這個(gè)符號，將公式用逗號隔開來表示公式（A1&...&Aμ）é（B1∨...∨Bv）。這樣在后繼式演算中，推理圖是由上層后繼式和下層后繼式構(gòu)成。其次，后繼式演算的推導(dǎo)是以基礎(chǔ)后繼式D—→D為初始后繼式的，而自然演繹是以假設(shè)公式作為初始公式。對推理圖進(jìn)行這些規(guī)范化之后，后繼式演算解決了“不可證”的問題，即對一個(gè)后繼式進(jìn)行證明，如果最終初始后繼式不是基礎(chǔ)后繼式的形式，則這個(gè)后繼式不可證，在自然演繹中這個(gè)問題并沒有得到解決。此外，經(jīng)過這樣的構(gòu)造使得證明具有更加優(yōu)美、完善的形式。特別是表現(xiàn)在古典邏輯中，由于LK演算推理圖中的后繼式后件可以包含多個(gè)S-公式。所以LK演算的推理圖具有對稱性，證明形式更加優(yōu)雅。

其次，后繼式演算系統(tǒng)的推理圖模式與自然演繹系統(tǒng)明顯不同。后繼式演算系統(tǒng)的推理圖，包括兩個(gè)部分，“算子推理圖”和“結(jié)構(gòu)推理圖”。甘岑不僅新添加了結(jié)構(gòu)推理圖，并且算子推理圖的形式也與自然演繹系統(tǒng)的推理圖有很大差別。甘岑這樣構(gòu)造推理圖，是出于提供一個(gè)標(biāo)準(zhǔn)化定理的證明為目的，即“切割消除定理”的證明。另一方面，這樣使得后繼式演算的形式更加簡潔、優(yōu)雅。算子推理圖盡管在形式上看起來與自然演繹系統(tǒng)的算子推理圖有很大差異，一是分了前件和后件規(guī)則，二是只有引入規(guī)則。但實(shí)際上與自然演繹系統(tǒng)推理圖的引入和消去系統(tǒng)的構(gòu)造方法一致，每個(gè)算子的后件引入規(guī)則對應(yīng)了自然演繹中的引入規(guī)則，其前件引入規(guī)則則對應(yīng)了自然演繹中的消去規(guī)則。

最后，LJ與LK演算的區(qū)別，和NJ與NK演算的差別看起來完全不同。NJ與NK演算的區(qū)別于是否包含排中律，而LJ與LK演算的區(qū)別則是規(guī)定了在LJ演算中，只允許推理圖中的后繼式后件至多包含一個(gè)S-公式，在LK中可包含多個(gè)S-公式。實(shí)際上LJ與LK演算的區(qū)別雖然表現(xiàn)在形式上，實(shí)際反映的區(qū)別與NJ與NK演算相同。通過對LJ進(jìn)行限制，排中律A∨?A排除在了LJ系統(tǒng)之外，在LK中，排中律A∨?A則可以得到證明。在LK中甘岑給出了“—→A∨?A”的證明［1］297：

但在LJ中，后繼式后件至多包含一個(gè)S-公式，因此我們只能進(jìn)行到以下步驟：

初始后繼式不是基礎(chǔ)后繼式的形式，因此，在LJ系統(tǒng)中“—→A∨?A”不可證。

2.2系 統(tǒng)中證明過程比較

從形式上來看，后繼式演算系統(tǒng)與自然演繹系統(tǒng)的證明都是樹形的，非循環(huán)的。但是二者在形式上存在很大的差別。以（?$xFx）é（"yFy）的證明為例：

在LJ系統(tǒng)中的證明［1］297：

在NJ系統(tǒng)中的證明［1］294：

第一，在后繼式演算中，證明中的推理圖是由后繼式構(gòu)成的；而自然演繹中的推理圖是由公式構(gòu)成的。第二，后繼式演算證明是以D—→D的基礎(chǔ)后繼式開始，稱為初始后繼式，在整個(gè)證明中沒有假設(shè)；自然演繹證明則是由假設(shè)公式作為初始公式，對初始公式?jīng)]有規(guī)定標(biāo)準(zhǔn)的形式，因而自然演繹的證明形式與后繼式演算相比不夠標(biāo)準(zhǔn)。第三，后繼式演算中引入結(jié)構(gòu)推理圖，使得證明更加標(biāo)準(zhǔn)，其中特殊的切割規(guī)則，會(huì)使一個(gè)公式“消失”，在這個(gè)例子中消去的是$xFx，仍然保持了子公式性質(zhì)，但是，由于推理圖中公式D是任意的，切割規(guī)則消去的可能是結(jié)論后繼式中S-公式的子公式之外的公式，也就是說可能會(huì)破壞子公式性質(zhì)；自然演繹系統(tǒng)中沒有結(jié)構(gòu)推理圖，仍然保持子公式性質(zhì)。在后繼式演算中，切割規(guī)則雖然會(huì)破壞子公式性質(zhì)，但是甘岑證明了“切割消除定理”，即每一個(gè)后繼式演算中的推導(dǎo)，都可以轉(zhuǎn)化為有同一個(gè)尾后繼式的沒有切割規(guī)則出現(xiàn)的推導(dǎo)。而子公式性質(zhì)作為一個(gè)推論也得以證明，即在一個(gè)沒有切割規(guī)則出現(xiàn)的后繼式演算推導(dǎo)中，出現(xiàn)的所有D-S-公式都是出現(xiàn)在尾后繼式（Endsequent）中的S-公式的子公式。

根據(jù)子公式性質(zhì)，加之后繼式演算的標(biāo)準(zhǔn)證明形式，我們可以在后繼式演算推導(dǎo)中進(jìn)行“證明搜索”。即當(dāng)我們給出一個(gè)后繼式需要在后繼式演算中證明的時(shí)候，這個(gè)后繼式作為樹形的“根”出發(fā)向上進(jìn)行搜索，如果這個(gè)推導(dǎo)可以一直進(jìn)行搜索直至它的每一個(gè)支都以“D—→D”的基礎(chǔ)后繼式結(jié)束，那么這個(gè)后繼式在后繼式演算系統(tǒng)中就是可證的。反之，如果我們進(jìn)行搜索時(shí)以非D—→D形式的后繼式結(jié)束，那么這個(gè)后繼式在后繼式演算系統(tǒng)中就是不可證的。例如我們之前的排中律的證明，在LK系統(tǒng)中對后繼式“—→A∨?A”進(jìn)行搜索，最終以“A—→A”結(jié)束，因此該后繼式在LK系統(tǒng)中可證，也就是排中律包含在LK系統(tǒng)之中。

在LJ系統(tǒng)中，我們進(jìn)行了所有可能的嘗試，對后繼式“—→A∨?A”進(jìn)行搜索，但是兩個(gè)推導(dǎo)分別以“—→A”和“A—→”結(jié)束，因此該后繼式在LJ系統(tǒng)中不可證，也就是說LJ系統(tǒng)將排中律排除在外。

證明搜索是后繼式演算系統(tǒng)特有的，我們可以提供可證和不可證的證明。自然演繹系統(tǒng)中我們可以證明一個(gè)系統(tǒng)內(nèi)的定理，但是如果一個(gè)定理在自然演繹系統(tǒng)中不可證，那么它的推導(dǎo)會(huì)陷入循環(huán)，無法停止，因此自然演繹系統(tǒng)無法給出一個(gè)系統(tǒng)外定理的不可證的證明。

此外，如果在LK演算中去掉é-IS（é的后件引入規(guī)則）和é-IA（é的前件引入規(guī)則），LK演算則具有對偶的特殊性質(zhì)。假設(shè)一個(gè)不包含é-IS和é-IA的LK推導(dǎo)，我們將其所有的后繼式做如下的轉(zhuǎn)換：將A1，...，Aμ—→B1，...，Bv轉(zhuǎn)換為Bv，...，B1—→Aμ，...，A1；將有兩個(gè)上層后繼式的推理圖，將兩個(gè)上層后繼式包括它們各自的推導(dǎo)進(jìn)行左右轉(zhuǎn)換；并將所有的&替換為∨，"替換為$，∨替換為&，$替換為"（在&與∨的互相替換中，要將其命題變元也進(jìn)行轉(zhuǎn)換，如A&B用B∨A替換）。這樣替換之后我們會(huì)發(fā)現(xiàn)這個(gè)對偶性質(zhì)，以&-IS為例：

進(jìn)行轉(zhuǎn)換后：

這時(shí)我們會(huì)發(fā)現(xiàn)，進(jìn)行左右的轉(zhuǎn)換之后，&-IS轉(zhuǎn)變?yōu)椤?IA。以此類推，其余的推理圖也可以進(jìn)行這種轉(zhuǎn)換，因此只有LK演算具有這樣的對偶性質(zhì)，進(jìn)而充分說明LK演算的證明具有對稱性。

綜上，甘岑的后繼式演算系統(tǒng)是對自然演繹系統(tǒng)的擴(kuò)展，基于提供“切割消除定理”的證明這一目的，甘岑構(gòu)造出了形式上更加標(biāo)準(zhǔn)，更加完善的邏輯演算。相比自然演繹系統(tǒng)，第一，后繼式演算系統(tǒng)將結(jié)論由一個(gè)公式拓展為多重結(jié)論，即后繼式；第二，在推導(dǎo)中規(guī)定了基礎(chǔ)后繼式“D—→D”為初始后繼式；第三，構(gòu)造了“結(jié)構(gòu)推理圖”和“算子推理圖”兩種推理圖，并且將自然演繹系統(tǒng)的引入和消去模式，以前件和后件的形式進(jìn)行的繼承和完善；第四，為“切割消除定理”提供了一個(gè)完整的證明，得出了子公式性質(zhì)這個(gè)推論。第五，基于以上，后繼式演算產(chǎn)生了“證明搜索”的性質(zhì)，可以提供一個(gè)后繼式可證和不可證的證明。至此，甘岑成功地構(gòu)造了后繼式演算系統(tǒng)，彌補(bǔ)了自然演繹系統(tǒng)的不足，證明了這個(gè)邏輯演算系統(tǒng)的合理性。

3　總結(jié)與展望

邏輯學(xué)與數(shù)學(xué)的結(jié)合，即用數(shù)學(xué)的研究方式研究邏輯推理，是現(xiàn)代邏輯發(fā)展的標(biāo)志。弗雷格借鑒了數(shù)學(xué)的形式系統(tǒng)構(gòu)造方法，創(chuàng)造了一套屬于邏輯學(xué)的形式語言，即“概念文字”，并且分別構(gòu)建了命題邏輯和謂詞邏輯的形式化的公理系統(tǒng)。邏輯學(xué)以“概念文字”為開端，運(yùn)用數(shù)學(xué)的研究方法來研究推理，數(shù)理邏輯應(yīng)運(yùn)而生，初步實(shí)現(xiàn)了傳統(tǒng)邏輯到現(xiàn)代邏輯的轉(zhuǎn)變。希爾伯特與他的學(xué)生阿克曼在弗雷格“概念文字”的基礎(chǔ)上，繼懷特海和羅素的《數(shù)學(xué)原理》之后，在《數(shù)理邏輯基礎(chǔ)》一書中對弗雷格的命題邏輯和謂詞邏輯的形式系統(tǒng)進(jìn)行了完善，構(gòu)造了“希爾伯特式的公理系統(tǒng)”?；谶@樣一套完整的形式系統(tǒng)，構(gòu)建的形式證明更加優(yōu)美，對證明論的發(fā)展也具有里程碑的歷史意義，因此希爾伯特被譽(yù)為數(shù)理邏輯和證明論的奠基人之一。

弗雷格、羅素和希爾伯特構(gòu)建的形式系統(tǒng)，借鑒了數(shù)學(xué)的公理系統(tǒng)，以公理和規(guī)則為基礎(chǔ)，其形式證明在甘岑看來，實(shí)際上遠(yuǎn)離了數(shù)學(xué)證明中使用的演繹形式。因此繼希爾伯特和阿克曼之后，甘岑在《邏輯演繹研究》中提出了“自然演繹”的概念。自然演繹是一種證明演算，在這種邏輯演算中，沒有公理，只包含推理規(guī)則，其推導(dǎo)從假設(shè)開始，更加接近自然的實(shí)際推理。甘岑的“自然演繹”則是繼弗雷格之后的又一次“驚艷”的創(chuàng)造。它突破了公理系統(tǒng)的模式，給我們提供了一種更接近實(shí)際推理的證明系統(tǒng)。“自然演繹”系統(tǒng)的構(gòu)造，不僅是現(xiàn)代邏輯史上，同時(shí)也是證明論史上的又一個(gè)里程碑。

在自然演繹系統(tǒng)的基礎(chǔ)上，甘岑針對其不足進(jìn)行了進(jìn)一步的完善，構(gòu)造了后繼式演算系統(tǒng)。其優(yōu)勢主要體現(xiàn)在兩個(gè)方面，一方面是經(jīng)過對自然演繹的擴(kuò)展，基于這個(gè)完整的形式系統(tǒng)，甘岑為“切割消除定理”構(gòu)造了完整的證明，得出了“子公式性質(zhì)”。另一方面，基于子公式性質(zhì)，和對形式證明的規(guī)范，后繼式演算具有的“證明搜索”的特性。在后繼式演算中可以對任意公式的后繼式根據(jù)推理規(guī)則向上進(jìn)行搜索，并且搜索可以停止。如果搜索以基礎(chǔ)后繼式“D—→D”作為結(jié)束，那么這個(gè)后繼式在系統(tǒng)內(nèi)是可證的，如果以基礎(chǔ)后繼式以外的后繼式結(jié)束，則不是系統(tǒng)內(nèi)可證的，解決了自然演繹的不可證問題。至此，甘岑完整的構(gòu)造了他的邏輯演算系統(tǒng)，并證明了該系統(tǒng)的合理性，在現(xiàn)代邏輯史上和證明論史上邁出了劃時(shí)代的一步。

甘岑的《邏輯演繹研究》對數(shù)理邏輯和證明論的發(fā)展具有深遠(yuǎn)的影響，繼甘岑之后，眾多國外的學(xué)者發(fā)展了它的邏輯演繹思想?！翱贫嗄埽∣iva Ketonen芬蘭）和克里（Haskell B.Curry美國）擴(kuò)展了對后繼式演算的處理，舒特（Kurt Schütte）將甘岑的切割消除定理轉(zhuǎn)移到通常的邏輯演算。洛倫茲（Paul Lorenzen）和舒特運(yùn)用“無窮歸納”研究了切割消除定理在證明論中的應(yīng)用。后來竹內(nèi)外史（Gaisi Takeuti日本）將甘岑演算推廣到一個(gè)能夠使實(shí)數(shù)理論形式化的類型論系統(tǒng)。雖然竹內(nèi)外史沒有證明切割消除定理，但是他證明假定廣義切割消除定理可以得出他的系統(tǒng)的一致性?！保?］288因此，甘岑的邏輯演繹思想在現(xiàn)代邏輯史上和證明論史上占有十分重要的地位，為現(xiàn)代邏輯和證明論的發(fā)展提供了方向，具有里程碑式的歷史價(jià)值。

［1］Gentzen G.Investigations into logical deduction［J］.American Philosophical Quarterly，1964（1）:4.

Comparative Analysis to Gentzen’s Subsequent Calculus System and Natural Deduction System

DONG Wen-yuan
（College of Information，Shanxi Agricultural University，Taigu，Shanxi030800，China）

Gerhard Gentzen’s inaugural dissertation for the University of G?ttingen，Investigations into Logical Deduction（Untersuchungen über das Logische Schliessen），in which he developed two forms of logic deduction，the natural deduction and subsequent calculus.Gentzen introduced his work by starting first from a natural deduction，which is closing to the the actual reasoning in mathematical proofs，and by then transforming it to a subsequent calculus，in which Gentzen gave a proof of the consistency of this system. Gentzen present his thought of logic deduction in this paper，and made a deeper work on the logic calculus. Gentzen’s thought of logic deduction is the milestone in the history of logic，and the study on his theory still has has great theoretical value and significance.This paper briefly describes the structure of Gentzen’s subsequent calculus’system，furthermore，the author makes a comparative analysis to subsequent calculus and natural deduction.

Natural Deduction；Subsequent Calculus；Logic Calculus System

B81

A

2096-0239（2016）03-0066-06

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

2016-05-11

中央高?；究蒲袠I(yè)務(wù)費(fèi)專項(xiàng)資金一般項(xiàng)目“達(dá)米特直覺主義邏輯演繹研究”，項(xiàng)目編號：SWU1609140。

董文媛（1989-），女，山西太原人，山西農(nóng)業(yè)大學(xué)信息學(xué)院創(chuàng)意寫作中心教師，碩士。研究方向：哲學(xué)邏輯與邏輯哲學(xué)。