自然演繹

自然演繹是證明論中嘗試提供象“自然”發生一樣的邏輯推理形式模型的一種方式。這種方式對比於使用公理的公理系統。

動機

自然演繹來源自對共通於弗雷格、羅素和希爾伯特系統的判句公理化(希爾伯特演繹系統)的不滿。這種公理化最著名使用是在羅素和懷特海的《數學原理》的數學論述中。在1926年由揚·武卡謝維奇在波蘭發起的一系列研討會提倡一種對邏輯的更加自然處理，斯坦尼斯瓦夫·亞希科夫斯基做了定義更自然的演繹的最早嘗試，首先在1929年使用了一種圖表表示法，並在1934年和1935年的一序列論文中更改了他的提議。但是他的提議沒有流行起來。現代形式的自然演繹是由德國數學家格哈德·根岑於1935年在一篇提交給哥廷根大學數學系的學位論文中獨立提出的。術語自然演繹就是在那篇論文中出現的:
首先我希望構造儘可能緊密於實際推理的一種形式化主義。所以提議了“自然演繹演算”。
—Gentzen,《UntersuchungenüberdaslogischeSchließen》(MathematischeZeitschrift39,pp.176-210,1935)
根岑被建立數論的一致性證明的目標所推動，因而找到了他的自然演繹演算的直接使用。但他不滿意自己證明的複雜性，並在1938年使用他的相繼式演算給出了一個新的一致性證明。在1961年和1962年的一系列研討會中，DagPrawitz給出了自然演繹演算的全面總結，並把根岑對相繼式演算做的很多工作轉運到了自然演繹框架中。他在1965年的專著《Naturaldeduction:aproof-theoreticalstudy》成為關於自然演繹的權威著作，並包括了模態和二階邏輯的套用。
在本文中提供的系統是根岑或Prawitz的公式化的一個小變體，但忠實於PerMartin-Löf對邏輯判斷和連結詞的描述(Martin-Lof,1996)。
[編輯]

判斷和命題

判斷是可知的事物，就是說知識的對象。如果有人實際上知道它則它是顯然(有證據的)的。所以"正在下雨"是一個判斷，對於知道實際上正在下雨的人而言它是顯然的；在這種情況下，你可以通過看窗外或走出屋子來輕易的找到這個判斷的證據。但是在數理邏輯中，證據通常不是直接可觀測到的，而是從更加基本的顯然判斷演繹來的。演繹的過程構成了一個證明；換句話說，一個判斷是顯然的，如果你有對它的證明。
在邏輯中最重要的判斷是“A為真”這種形式的。字母A表示代表一個命題的任何表達式；這個真理判斷要求更基本的判斷:“A是命題”。很多其他判斷也已經被研究了；比如“A為假”(參見經典邏輯)，“A在時間t為真”(參見時間邏輯)，“A必然為真”或“A可能為真”(參見模態邏輯)，“程式M有類型τ”(參見程式語言和類型論)，“A從可用的資源是可完成的”(參見線性邏輯)，等等。作為開始，我們先只關注最簡單的兩個判斷“A是命題”和“A為真”，分別縮寫為“Aprop”和“Atrue”。
[編輯]

形成規則

判斷“Aprop”定義了A的有效證明的結構，它們進而定義了命題的結構。出於這個原因，判斷的推理規則有時叫做形成規則。作為展示，如果我們有兩個命題A和B(就是說，判斷“Aprop”和“Bprop”是顯然的)，則我們形成了複合命題A與B，符號化寫為""。我們可以用推理規則的形式把它寫為:
這個推理規則是“模式性”的:A和B可以示例任何表達式。推理規則的一般形式為:
這裡的每個都是一個判斷，而推理規則被命名為“name”。橫線上的判斷叫做前提，而橫線下的判斷叫做結論。其他常見的邏輯命題是析取()，否定()，蘊涵()，和邏輯永真()和永假()。它們的形成規則如下。

介入和除去規則

現在我們討論“A為真(是真理)”判斷。在本文餘下部分中，我們將在已被理解的地方省略“prop”判斷。在結論中介入邏輯連結詞的推理規則叫做介入規則。要介入合取，就是說從命題A和B推導出“AandB為真”，你需要“A為真和B為真”的證據。作為一個推理規則:
上述規則實際上是省略命題判斷的簡寫[1]。
在空無(nullary)的情況下，你可以從沒有前提中推導出真理。
注意在空無的情況下，對於虛假是沒有介入規則的。所以你永遠不能從更簡單的判斷推導出虛假。
如果一個命題的真實性可以通過多於一種方式來確立，則相應的連結詞有多個介入規則。
對偶於介入規則的是描述如何把關於複合命題的信息解構為關於它的成員的信息的除去規則。因此，從“A∧B為真”，我們可以推導出“A為真”和“B為真”:
我們已經見到的推理不足以陳述蘊涵介入或析取除去的規則；為此我們需要假言推導的更一般的概念。

例子

作為推理規則的使用例子，考慮合取的交換律。如果A∧B為真，則B∧A為真；這可以通過以底下推理的前提匹配上面推理的結論的方式構成推理規則來完成這種推導。

假言推導

在數理邏輯中普遍性的操作是“依據假定的推理”。例如，考慮下列推導:
這個推導不確立B為真；而確立了下列事實:
如果“A∧(B∧C)true”則“Btrue”。
在邏輯中，我們讀做“假定A∧(B∧C)為真，我們證實B為真”；換句話說，判斷“Btrue”依賴於假定的判斷“A∧(B∧C)true”。這叫做假言推導，它可寫為如下:
釋義為:“Btrue”推導自“A∧(B∧C)true”。當然，在這個特定的例子中我們實際上知道“Btrue”來自“A∧(B∧C)true”的推導，但是一般而言，我們不可以先驗的知道這個推導。假言推導的一般形式為:
每個假言推導都有寫在頂行的一組前件推導(Di)，和寫在底行的一個後件判斷(J)。每個前提自身都可以是一個假言推導。(出於簡單性，我們把這種判斷處理為無前提推導。)

推理規則

假言判斷的概念被主觀化為蘊涵的連結詞。蘊涵介入規則和蘊涵除去規則如下。
在介入規則中，命名為u的前件被“注入”到結論中。這是界定假設的範圍的機制:它存在的唯一理由是確立“Btrue”；它不能被用做任何其他目的，特別是，它不能被用在這個介入之下。作為一個例子，考慮“A(B(A∧B))true”的推導:
這是個沒有不滿足前提的完整推導；但是，子推導是假設的。例如“B(A∧B)true”的推導假設了前件“Atrue”(命名為u)。
通過假言推導，我們現在寫出析取除去規則:
用口語說，如果“A∨Btrue”，並且我們可以從“Atrue”和“Btrue”二者推出“Ctrue”，則確實“Ctrue”。注意這個規則不依靠於“Atrue”或“Btrue”中的任何一個。
在空無的情況下，我們得到下列有關虛假的除去規則:
這讀做:如果虛假為真，則任何命題C為真。
否定介入規則和否定除去規則類似於蘊涵。
介入規則注入了假設u的名字。因為這些規則是模式性的，介入規則的釋義為:如果我們可以從“Atrue”推導出“Ptrue”和“¬Ptrue”，就是；則A必定為假，也就是“¬Atrue”。對於除去規則，如果A和¬A二者都被證明為真，則這是個矛盾，在這種情況下所有命題C為真。因為蘊涵和否定的規則如此的類似，很容易看出¬A和A⊥是等價的，就是可以相互推導的。

一致性，完備性和規範形式

一個理論被稱為是一致(相容)的，如果虛假(從沒有前提)是不能證明的，被稱為是完備的，如果所有定理都可以使用這個邏輯的推理規則來證明。這是關於整體的邏輯的陳述，並通常和某種模型的概念聯繫在一起。但是，還有對推理規則的純粹語法檢查的一致性和完備性的局部的概念，而不需要訴諸模型。首先是局部一致性，也叫做還原性，它聲稱包含了一個連結詞的介入、並立即跟隨著它的除去的任何推導都可以被轉換成不包含這種迂迴的等價推導。這是對除去規則力量的檢查:它們不能強大得包含了在前提中沒有包含的知識。作為一個例子，考慮合取。
⇒
作為對偶，局部完備性聲稱除去規則足夠強大來把一個連結分解成適合它的介入規則的形式。再次考慮合取:
⇒
使用Curry-Howard同構，除去規則和介入規則分別精確的對應於lambda演算中的β-歸約和η-展開。通過局部完備性，我們看到所有推導都可以被轉換成介入主要連結詞的等價推導，實際上，如果整個推導都服從除去跟隨著介入的這種次序，則可以被稱為是規範的。在規範推導中，所有除去都出現在介入上面。在大多數邏輯中，所有推導都有等價的規範推導，叫做規範形式。規範形式的存在使用自然演繹自身一般是難於證明的，這種理由確實存在於文獻中，其中最著名的是DagPrawitz1961年的書《Naturaldeduction:aproof-theoreticalstudy》，A&WStockholm1965,沒有ISBN。通過免切相繼式演算表達的方式做間接的證明是非常容易的。

一階擴展

一階系統總結
前面章節中的邏輯是“單類”邏輯的例子，單類邏輯只帶有單一一類對象:命題。已經提出了對這個簡單框架的很多擴展；在本章中我們將向它擴展上第二類對象：個體或項。更精確地說，我們將增加新的一類判斷“t是項”(或“tterm”)，這是的t是模式性的。我將固定一個變數的可數集合V，函式符號的可數集合F，並如下這樣構造項:
對於命題，我們考慮第三個謂詞的可數集合。並用如下規則定義“在項之上的原子謂詞”:
此外，我們增加一對“量化的”命題:全稱()和存在():
這些量化的命題有如下的介入和除去規則。
在這些規則中，符號[t/x]A表示代換A中x的所有(可見)實例為t，避免它被其他量詞捕獲；關於這種標準操作的詳細描述請參見lambda演算。同前面一樣，名字上的上標表示被注入的成分:在的結論中不能出現項a(這種項叫做本徵變數或參數)，在中指名為u的假設被局部化到假言推導的第二個前提中。儘管早先章節中的命題邏輯是可判定的，增加量詞使邏輯成為不可判定的。

高階擴展

迄今為止量化擴展是“一階的”:它們用把命題區別於在其上量化的對象的種類。高階邏輯採用了一種不同的方式，它只有一個種類的命題，量詞的量化範圍是同種類的命題，反映於形成規則:
關於高階邏輯的介入和除去規則的討論超出了本文的範圍。有介於一階和高階邏輯之間的邏輯。例如，二階邏輯有兩類命題，第一類量化於項，第二類量化於第一類命題之上。

證明論

迄今為止對自然演繹的表述集中於命題的本質而沒有給出證明的形式定義。要形式化證明的概念，我們要稍微更改假言推導的表述。我們向前件標籤上證明變數(來自某個變數的可數集合V)，並用實際證明裝飾後件。通過十字轉門(turnstile)的方式把前件或假設同後件分隔開。這種修改有時叫做局部化假設。下列圖示總結變更。
⇒
假設的蒐集將被寫為Γ，當它們的精確內容是無關的時候。要使證明直接了當，我們把無關證明的判斷“Atrue”換成判斷“π是證明(Atrue)”，它在符號上被寫為“π:Atrue”。服從標準方式，證明用它們自己的對“πproof”的形成規則來指定。最簡單的可能的證明是使用帶標籤的假設；在這種情況下證據是標籤自身。
為了簡短，我們在本文餘下部分去掉判斷標籤“true”，就寫為“Γπ:A”。讓我們通過明確的證明來重新檢驗某些連結詞。對於合取，我們查看介入規則∧I來發現合取的證明形式:它們必須是兩個合取項的一對證明。就是:
除去規則∧E1和∧E2選擇要么左面的要么右面的合取項；所以證明是一對投影—第一個(fst)和第二個(snd)。
對於蘊涵，介入形式的局部化或約束，書寫要使用λ；這對應於注入標籤。在規則“Γ,u:A”中表示一組假設Γ，同增補的一個假設u在一起。
通過明確可用的證明，你可以操縱和思辯證明。證明的關鍵操作是用一個證明去替換在另一個證明中使用的假定。這通常叫做“代換定理”，並可以通過關於第二個判斷的深度(或結構)的歸納法證明。
代換定理
如果並且,則。

類型論

迄今為止判斷“Γπ:A”有一個純邏輯釋義。在類型論中，邏輯觀點被調換為更加可計算的對象的觀點。在邏輯釋義中的命題現在被看作類型，而證明被看作使用lambda演算寫的程式。所以“π:A”的釋義是“程式π有類型A”。邏輯連結詞也有不同的讀法:合取被看作乘積(×)，蘊涵被讀做函式箭頭(→)等等。區別只是裝飾。類型論有使用形成、介入和除去規則的自然演繹表示；事實上，讀者可以用前面的章節重新構造一個“簡單的類型論”。
在邏輯和類型論之間的區別主要是把焦點從類型(命題)轉移到了程式(證明)。類型論主要感興趣於程式的可轉換性和可歸約性。對於所有類型，都有這個類型的一個不可歸約的規範程式；它們叫做“規範形式”或“值”。如果每個程式都可以歸約到規範形式，則這個類型論被成為是“規範化”的(或“弱規範化”的)。如果規範形式是唯一性的，則這個理論被稱為“強規範化”的。可規範化性是多數非平凡的類型論所稀有的特徵，這是對邏輯世界的巨大違背。(回想起所有邏輯推導都有一個等價的正規推導)。概述其理由:在接受遞歸定義的類型論中，有可能寫出用不歸約到一個值的程式；比如循環程式一般可以給予任何類型。特別是，有類型⊥的循環程式，儘管沒有“⊥true”的邏輯證明。為此，“命題為類型；證明為程式”範例只在一個方向上成立:把一個類型論解釋為邏輯一般會給出一個不一致的邏輯。
象邏輯一樣，類型論也有很多擴展和變體，包括一階和高階版本。叫做依賴類型論的一個有趣的類型論分支允許量詞設定範圍於在程式自身上。這些量化的類型被寫為Π和Σ替代和，並有如下形成規則:
這些類型分別一般化了箭頭和乘積類型，通過它們的介入和除去規則。
完全一般性的依賴類型論是非常強力的:它可以把幾乎所有程式的可想像的性質直接表達為程式的類型。這種一般性來自於高代價—檢查一個給定程式是否有給定類型是不可判定的。為此，依賴類型理論在實踐中不允許在任意程式上的量化，而是限制於給定的可判定的“索引域”的程式，例如整數，字元串或線性程式。
因為依賴類型論允許類型依賴於程式，有一個自然的問題要問，程式依賴於類型或者任何其他組合是否是可能的。對這個問題有很多種回答。類型論中一個流行的方式是允許程式量化在類型上，也叫做“參數多態”；這還有兩個主要的種類:如果類型和程式保持分離，則得到更好行為的系統，叫做“直謂多態”；如果在程式和類型之間的區別被模糊了，將得到高階邏輯的類型論對應，叫做“非直謂多態”。文獻中已經考慮了依賴性和多態性的各種組合，最著名的是HenkBarendregt的lambda立方。
邏輯和類型論的交集是廣闊和活躍的研究領域。新邏輯通常以類型論架構來形式化，這叫做邏輯框架。流行的現代邏輯框架比如構造演算和LF是基於高階依賴類型論，帶有在可決定性和表達能力上的各種妥協。這些邏輯框架自身總是規定為自然演繹系統，這是對自然演繹方式的多功能性的明證。

經典邏輯

為了簡單性，迄今為止提出的邏輯都是直覺的。經典邏輯向直覺邏輯擴展了補充的排中律公理或原理。
對於任何命題p，命題p∨¬p為真。
這個陳述沒有明顯的介入和除去；實際上，它涉及兩個不同連結詞。Gentzen對排中律的最初處理規定了它是下列三個(等價)的公式之一，它們在希爾伯特和Heyting的系統中已經已類似形式存在了:
排中律的這種處理，除了被純粹主義者所反對之外，把額外的複雜介入到了規範形式的定義中。
相對更加另人滿意的以單獨的介入和除去規則處理經典自然演繹首次由Parigot在1992年提出，採用了叫做λμ的lambda演算的形式。他的方式的關鍵性洞察是把真理中心的判斷Atrue替代為更加經典的概念:在局部化形式中，不再使用ΓA，他使用ΓΔ，而Δ是類似於Γ的一個命題的蒐集。Γ被處理為一個合取，而Δ是一個析取。這種結構本質上是直接從經典的相繼式演算轉移過來的，但是革新為λμ給予了經典自然演義證明一種計算性的意義，通過在LISP和它的後代中可見到的callcc或throw/catch機制的方式。(參見:一級控制)。

模態邏輯

另一個重要擴展是模態和其他不只需要基本的真理判斷的邏輯。它們由Prawitz在1965年以自然演繹的樣式首次描述，並累積了大量有關的工作。給出一個簡單的例子，必然性的模態邏輯需要一個新判斷，“Avalid”，它是無條件的真理:
如果“Atrue”不在形如“Btrue”的假定之下，則“Avalid”。
這個無條件判斷被主觀化為一元連結詞A(讀做“必然性的A”)，帶有如下的介入和除去規則:
注意前提“Avalid”沒有定義規則；有效性的無條件定義替代了它的位置。這個模式在局部化形式中變得更加清楚，這時假設是明確的。我們寫“Ω;ΓAtrue”，這裡的Γ象以前一樣包含真假定，而Ω包含有效假定。在右面只有一個單一的判斷“Atrue”；這裡不需要有效性，因為“ΩAvalid”被定義為同於“Ω;Atrue”。介入和除去形式為:
模態假設有自己版本的假設規則和代換定理。
模態代換定理
如果並且,則。
把判斷分解到不同假設蒐集中的這種框架也叫做“多區”或“多價”上下文，是非常強力和可擴展性的；它已經被用於很多不同的模態邏輯[5]，線性邏輯[6]和其他亞結構邏輯中。

同相繼式演算比較

主條目：相繼式演算
相繼式演算是自然演繹作為數理邏輯基礎的主要替代者。在自然演繹中信息流是雙向的:除去規則流向下解構，而介入規則流向上構造。所以，自然演繹證明不能純粹自上而下或自下而上的閱讀，這使得它不適於證明查找的自動化，甚至不適於證明檢查(或類型論中類型檢查)。為此，根岑在1935年提出了他的相繼式演算，他最初打算把它作為澄清謂詞邏輯的一致性的技術手段。克萊尼在1952年於著作《IntroductiontoMetamathematics》(ISBN0720421039)中，給出了相繼式演算的第一個現代樣式的形式化。
在相繼式演算中，所有推理規則都可以純粹的自底向上的閱讀。推理規則可以套用於十字轉門兩側的元素之上。(為了區分於自然演繹，本文對相繼式使用雙箭頭⇒來替代。自然演繹的介入規則被看作相繼式演算中“右規則”，並且在結構上非常類似。在另一方面除去規則對應相繼式演算中“左規則”。作為例子，考慮析取；右規則是常見的:
而左規則:
讓人想起局部化形式的自然演繹的∨E規則:
命題A∨B，是在∨E中的一個前提的後件，轉變成在左規則∨中結論的一個假設。所以，左規則可以被看作某種反向的除去規則。
在相繼式演算中，左和右規則銜接著(lock-step)進行，直到到達初始相繼式，它對應於自然演繹中除去規則和介入規則的匯合點。這些初始化規則粗淺的類似於自然演繹的假設規則，但是在相繼式演算中它們描述左和右命題的換位(transposition)或“握手”:
在相繼式演算和自然演繹之間的對應是一對可靠性和完備性定理，它們都是可以通過歸納論證來證明的。
關於的可靠性
如果,則。
關於的完備性
如果,則。
很明顯通過這些定理，相繼式演算不改變真理的概念，因為同一組命題仍然是真的。所以，你可以使用同樣的證明對象，如以前在相繼式推導中一樣。作為例子，考慮合取。右規則實質上等同於介入規則
相繼式演算 自然演繹
但是，左規則進行了在相應的除去規則中不進行的額外替換。
相繼式演算 自然演繹
所以在相繼式演算中生成證明的種類和從自然演繹中生成的是相當不同的。相繼式演算生成的證明叫做“β-正規η-長”形式，它對應於自然演繹證明的正規形式的規範表示。如果你嘗試使用自然演繹自身來描述這些證明，你將得到所謂的“插入演算”(由JohnByrnes[3]首先描述的)，它可以用來形式化的定義自然演繹的“正規形式”的概念。
自然演繹的代換定理在相繼式演算中採用了結構規則或叫做切的結構定理的形式。
切(代換)
如果並且,則。
在多數有良好行為的邏輯中，切作為推理規則不是必需的，儘管它仍是可證明為一個元定理；切規則的多餘通常表現為一個計算過程，叫做“切除去”。這是自然演繹的一個有趣的套用；通常直接在自然演繹中證明特定性質是非常冗長的，因為有無限制數目的情況。例如，考慮證明給定的命題在自然演繹中是不可證明的。一個簡單歸納論證將失敗，因為規則如∨E或E，它們介入了任意的命題。但是，我們知道相繼式演算關於自然演繹是完備的，所以在自然演繹中證明這中不可證明性就足夠了。現在如果切不能獲得為一個推理規則，則所有相繼式規則要么介入一個連結詞於右側要么於左側，所以相繼式推導的深度完全受限於在最終結論中的連結詞。所以，證明不可證明性是非常容易的，因為只有有限數目的情況要考慮，而每個情況都完全由結論的子公式組成的。一個簡單的實例是“全局一致性”定理:“true”是不可證明的。在相繼式演算中，這明顯為真，因為沒有規則可以有“”作為結論!由於這個性質，證明論學者經常偏好免切相繼式演算公式化。