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

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

上一篇：證明論學習筆記1：預備知識

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

我們可以從滿足（satisfaction）和證明（proof）兩個角度來看待邏輯。而滿足和證明又可以一般化為後承關係（consequence relation）。

一般認為，語言 上的後承關係 滿足下面三個特徵：

• 包含（inclusion）：如果 那麼
• 單調性（monotonicity）： ，又稱弱化（weakening, thinning）
• 切（cut）：

被稱為相繼式（sequent），其中 被稱為前提（premises）， 被稱為結論（conclusion）。

邏輯的證明論描述被稱為邏輯的一個表示（representation）。在三種主要的邏輯表示模式中，我們先介紹希爾伯特系統（the Hilbert representation/system）。

在希爾伯特系統，公理（axioms）和推理規則（rules of inference）是兩大支柱。如果不需要任何前提就可以證明 ，即 ，那麼我們稱 為定理（theorems）。

經典命題邏輯的希爾伯特表示：

一、公理模式（axiom schemas）：

將框架中的命題符號替代為具體命題就構成了具體的公理。

如果捨棄公理3，我們就得到了正蘊含邏輯（positive implicational logic）。

二、推理法則：

肯定前件（modus ponens）：

上述表示方法只用到了運算元 和 ，因為其他運算元都可以通過這兩個運算元進行定義。

經典謂詞邏輯的希爾伯特表示：

一、公理框架（axiom schemes）：

1. 
2. 
3. 
4. 
5. ，如果 可以自由替換 （t is free for x in A）
6. ，如果 不包含自由出現的

在 中， 可以自由替換 ，但 不可以自由替換 。

二、推理法則：

1. 肯定前件（modus ponens）：

2. 推廣（generalization）：

肯定前件又被稱為箭頭消除法則（ ），推廣又被稱為全稱量詞引入法則 。

希爾伯特系統對應著組合子邏輯（combinatory logic）；而自然演繹和根岑的相繼式演算則直接對應著 演算。

• K 組合子對應著公理
• S 組合子對應著公理
• I 組合子對應著冗餘公理 ，因而組合子 I 也是冗餘（redundant）的（它和 S K K 是等價的，即外延相同）

組合子邏輯的簡單 Haskell 演示：

"λ" i x = xi :: p -> p"λ" k x y = xk :: p1 -> p2 -> p1"λ" s x y z = x z ( y z )s :: (t1 -> t2 -> t3) -> (t1 -> t2) -> t1 -> t3"λ" :t s k ks k k :: p1 -> p1"λ" :t ii :: p -> p"λ" s k k "JOHN""JOHN"it :: [Char]"λ" i "JOHN""JOHN"it :: [Char]

參考文獻：

Basic proof theory

Handbook of Logic in Computer Science

Hilbert system - Wikipedia

Hilbert system in nLab

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

上一篇：證明論學習筆記1：預備知識

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