證明論學習筆記4：直覺主義邏輯和相繼式演算

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

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

下一篇：證明論學習筆記5：賦值系統

在討論直覺主義邏輯之前，我們先看一下用相繼式演算（sequent calculus）表示的經典邏輯的自然演繹規則：

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

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

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

除了「雙重否定」之外，其餘的規則要麼是引入規則，要麼是消除規則，具有很好的對稱性。將「雙重否定」這一規則刪去，我們就得到了直覺主義邏輯 .

但值得注意的是，直覺主義邏輯否定的只是經典邏輯中 的一個方向。由於證明必須具有構造性，我們無法證明 ，但是卻可以證明 。先對 和 應用否定消除，得到 ，再應用否定引入規則，得到 ，而 恰恰是 的一未歸約式。

從實際證明的角度來講，有些自然演繹規則是很有用的，例如合取引入規則 。如果我們要找到 的證明，只需要分別找到 和 的證明就好了。但是，有些規則對於尋找證明來說幫助不大，例如合取消除規則。如果要證明「張三是老師」，沿著合取消除規則，我們可以證明「張三和李四是老師」。但「張三和李四是老師」的證明其實比「張三是老師」的證明更難。此外，我們也無法運用否定消除規則來證明 。

為此，根岑提出了一種新的子邏輯式概念（參見：證明論學習筆記1：預備知識）：

根岑子邏輯式（Gentzen subformula）：

• 是所有邏輯式的子邏輯式
• 是 和 的子邏輯式
• 和 是 和 的子邏輯式
• 如果 或 是 的子邏輯式，那麼 也是 的子邏輯式。其中 是所有不包含 的項。

定義（子邏輯式特性，subformula property）：

證明法則 擁有子邏輯式特性，如果 中的每一個邏輯式都是 中一個邏輯式的子邏輯式。

子邏輯式特性可以用來逆推證明。自然演繹規則里的引入規則都具備子邏輯式特性。但它的消去規則都不具備子邏輯式特性。為了確保子邏輯式特性，我們可以將消去規則刪除，增加新的一組引入規則，即在語境中引入邏輯運算符的規則，我們稱之為「左引入規則」，與之前介紹的引入規則（「右引入規則」）相對應。

簡而言之，如果引入的運算符出現在 左側，則為左引入規則，如果引入的運算符出現在 右側，則為右引入規則。根岑的 規則羅列如下：

結構規則（structural rules）：

• （包含）
• （切）
• （右單調）
• （左單調）

邏輯規則（logical rules）：

• 右合取：
• 左合取：
• 右析取：
• 左析取：
• 右箭頭：
• 左箭頭：
• 右否定：
• 左否定：
• 右全稱：
• 左全稱：
• 右存在：
• 左存在：

除了「切」之外，上述規則均滿足子邏輯式特性。根岑於是又提出了著名的「切消定理」，即所有用到切的證明均可用沒有用到切的證明來代替。

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

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

下一篇：證明論學習筆記5：賦值系統

參考文獻：

Basic proof theory

Handbook of Logic in Computer Science