在數理邏輯中，自然演繹是證明論中嘗試提供象“自然”發生一樣的邏輯推理形式模型的一種方式。這種方式對比於使用公理的公理系統。
基本介紹
- 中文名：自然演繹
- 外文名：natural deduction
動機,判斷和命題,形成規則,經典邏輯,
動機
自然演繹來源自對共通於弗雷格、羅素和希爾伯特系統的判句公理化(希爾伯特演繹系統)的不滿。這種公理化最著名使用是在羅素和懷特海的《數學原理》的數學論述中。在1926年由揚·武卡謝維奇在波蘭發起的一系列研討會提倡一種對邏輯的更加自然處理，斯坦尼斯瓦夫·亞希科夫斯基做了定義更自然的演繹的最早嘗試，首先在1929年使用了一種圖表表示法，並在1934年和1935年的一序列論文中更改了他的提議。但是他的提議沒有流行起來。現代形式的自然演繹是由德國數學家格哈德·根岑於1935年在一篇提交給哥廷根大學數學系的學位論文中獨立提出的。術語自然演繹就是在那篇論文中出現的:
首先我希望構造儘可能緊密於實際推理的一種形式化主義。所以提議了“自然演繹演算”。
— Gentzen, 《Untersuchungen über das logische Schließen》(Mathematische Zeitschrift 39, pp.176-210, 1935)
根岑被建立數論的一致性證明的目標所推動，因而找到了他的自然演繹演算的直接使用。但他不滿意自己證明的複雜性，並在1938年使用他的相繼式演算給出了一個新的一致性證明。在1961年和1962年的一系列研討會中，Dag Prawitz 給出了自然演繹演算的全面總結，並把根岑對相繼式演算做的很多工作轉運到了自然演繹框架中。他在1965年的專著《Natural deduction: a proof-theoretical study》成為關於自然演繹的權威著作，並包括了模態和二階邏輯的套用。
在本文中提供的系統是根岑或 Prawitz 的公式化的一個小變體，但忠實於 Per Martin-Löf 對邏輯判斷和連結詞的描述(Martin-Lof, 1996)
判斷和命題
是可知的事物，就是說知識的對象。如果有人實際上知道它則它是顯然(有證據的)的。所以"正在下雨"是一個判斷，對於知道實際上正在下雨的人而言它是顯然的；在這種情況下，你可以通過看窗外或走出屋子來輕易的找到這個判斷的證據。但是在數理邏輯中，證據通常不是直接可觀測到的，而是從更加基本的顯然判斷演繹來的。演繹的過程構成了一個證明；換句話說，一個判斷是顯然的，如果你有對它的證明。
在邏輯中最重要的判斷是“A 為真”這種形式的。字母 A 表示代表一個命題的任何表達式；這個真理判斷要求更基本的判斷:“A 是命題”。很多其他判斷也已經被研究了；比如“A 為假”(參見經典邏輯)，“A 在時間 t 為真”(參見時間邏輯)，“A 必然為真”或“A 可能為真”(參見模態邏輯)，“程式 M 有類型 τ”(參見程式語言和類型論)，“A 從可用的資源是可完成的”(參見線性邏輯)，等等。作為開始，我們先只關注最簡單的兩個判斷 “A 是命題”和“A 為真”，分別縮寫為“Aprop”和“A true”。
形成規則
判斷“A prop”定義了 A 的有效證明的結構，它們進而定義了命題的結構。出於這個原因，判斷的推理規則有時叫做形成規則。作為展示，如果我們有兩個命題 A 和 B (就是說，判斷“A prop” 和“B prop”是顯然的)，則我們形成了複合命題 A 與 B，符號化寫為 "
。我們可以用推理規則的形式把它寫為:
這個推理規則是“模式性”的: A 和 B 可以示例任何表達式。推理規則的一般形式為:
經典邏輯
為了簡單性，迄今為止提出的邏輯都是直覺的。經典邏輯向直覺邏輯擴展了補充的排中律公理或原理。
對於任何命題 p，命題 p ∨ ¬p 為真。
這個陳述沒有明顯的介入和除去；實際上，它涉及兩個不同連結詞。Gentzen 對排中律的最初處理規定了它是下列三個(等價)的公式之一，它們在希爾伯特和 Heyting 的系統中已經已類似形式存在了:
相對更加另人滿意的以單獨的介入和除去規則處理經典自然演繹首次由 Parigot 在 1992 年提出，採用了叫做 λμ 的lambda 演算的形式。他的方式的關鍵性洞察是把真理中心的判斷 A true 替代為更加經典的概念: 在局部化形式中，不再使用 Γ A，他使用 Γ Δ，而 Δ 是類似於 Γ 的一個命題的蒐集。Γ 被處理為一個合取，而 Δ 是一個析取。這種結構本質上是直接從經典的相繼式演算轉移過來的，但是革新為 λμ 給予了經典自然演義證明一種計算性的意義，通過在 LISP 和它的後代中可見到的 callcc 或 throw/catch 機制的方式。(參見: 一級控制)。
