證明論學習筆記3：自然演繹

目錄：類型論驛站寫作計劃

上一篇：證明論學習筆記2：希爾伯特系統

自然演繹（natural deduction）和希爾伯特系統的主要區別是沒有公理。由於不存在公理，在證明過程中，我們可以引入其他邏輯式作為假設。這些假設稍後可以被除去（discharge）。

自然演繹里的邏輯後承（consequence）關係定義如下： 如果存在 的基於前提 的自然演繹證明。

Ja?kowski 和 Prawitz 等人藉助方框（box）來描述自然演繹的推理規則：

經典邏輯的自然演繹規則

• 合取引入：
• 合取消除：
• 析取引入：
• 析取消除： （右側從A到C，從B到C應該用兩個方框括起來，因為排版限制，我臨時採用方括弧表示。）
• 箭頭引入：
• 箭頭消除：
• 否定引入： （實為箭頭引入之特例）
• 否定消除：
• 謬誤沒有引入規則
• 謬誤消除：
• 全稱引入： （我們隨便引入一個變數 ，如果我們可以證得 ，那麼由於我們對 是不加假設的，那麼我們可以證得結論。箭頭引入不過是帶類型的全稱引入（引入結果是 ）的特例，當 在 中不自由出現時，我們有 即為 。因此全稱引入乃根本大法。）
• 全稱消除：
• 存在引入：
• 存在消除：
• 雙重否定：

此外，在全稱引入和存在消除法則里， 不能在方框外出現。

命題 的自然演繹證明：

1. ，假設
2. ---- ，假設
3. ---- ，
4. ---- ，
5. ,
6. ，

Coq 證明流程示例：

Variables A B: Prop.Theorem example: ~ B -> (B -> A).Proof.intro notb.intro b.apply False_ind.elim notb.assumption.Qed.

自然演繹還可以用相繼式（sequent）的形式來表示，其優點是證明的過程會更為簡明易懂，而且排版也更為方便。

相繼式式的經典邏輯自然演繹規則

• 合取引入：
• 合取消除：

析取引入：

析取消除：

• 箭頭引入：
• 箭頭消除：
• 否定引入：
• 否定消除：
• 謬誤沒有引入規則
• 謬誤消除：
• 全稱引入：
• 全稱消除：
• 存在引入：
• 存在消除：
• 雙重否定：

在全稱引入中， 不能在 或 中自由出現；在存在消除中， 不能在 ， 或者 中自由出現。

參考文獻：

Handbook of Logic in Computer Science

目錄：類型論驛站寫作計劃

上一篇：證明論學習筆記2：希爾伯特系統

推薦閱讀：