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

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

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

證明論大致可以分為結構證明論（structural proof theory）和詮釋證明論（interpretational proof theory）。

其中結構證明論基於形式證明結構的組合分析，核心方法是切消除（cut elimination）和正規化（normalization）。

而詮釋證明論則經常將一個形式理論的句法翻譯成另一個形式理論，例如從經典邏輯到最小邏輯的哥德爾-根岑嵌入（G?del-Gentzen embedding）。

什麼是一階謂詞邏輯（first-order predicate logic）？

一階謂詞邏輯可以用來推理具體事物、事物之間的關係及其它們之間的邏輯關係。一階邏輯有多種具體的形式表述。我們採用的版本是：

取下列初始邏輯運算元（primitive logical operators）：

• 二元： （此三者參數均為命題）
• 零元：

取下列量詞（quantifiers），用來約束（bind）命題中的變數：

• 全稱量詞：
• 存在量詞：

又取可數無限個變數（variables）， 元關係（n-place relations），以及 元函數（n-ary functions）。零元關係被稱為命題變數，零元函數被稱為常量。原子式（atomic formulas）形如 。原子式加上 被稱為初始式（prime formulas）。

另外， 縮寫為 ； 縮寫為 。

替換、約束和自由變數

一個邏輯式中受到量詞約束的變數被稱為約束變數（bound variables），不受量詞約束的變數被稱為自由變數（free variables）。我們用 來表示項 中自由變數的集合。

用項 來替換（substitute ... for ...）表達式 中的變數 ，標記為 或 。用等量的項來替換等量的變數，可以使用向量標記法 。

子邏輯式（subformulas）

根岑子邏輯式（Gentzen -）：

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

直白子邏輯式（literal -）：

• 是 的子邏輯式。
• 如果 或 是 的子邏輯式，那麼 和 也是 的子邏輯式。
• 如果 或 是 的子邏輯式，那麼 也是 的子邏輯式

如不含修飾語，我們所指的子邏輯式一般為根岑子邏輯式

正、負、嚴格正子邏輯式：

• 是 的正（positive）和嚴格正（strictly positive）子邏輯式。
• 如果 或 為 的正[負，嚴格正]子邏輯式，那麼 和 也是相應類別的子邏輯式。
• 如果 或 是 的正[負，嚴格正]子邏輯式，那麼 也是 的相應類別的子邏輯式。其中 是所有不包含 的項。
• 如果 是 的正[負]子邏輯式，那麼 則是 的負[正]子邏輯式， 是 的正[負]子邏輯式。
• 如果 是 的嚴格正子邏輯式，那麼 也是 的嚴格正子邏輯式。
• 嚴格正子邏輯式又被稱為嚴格正部分（strictly positive part, s.p.p.）。
• 的子邏輯式的集合為所有正子邏輯式和所有負子邏輯式的並集。

語境（contexts）：

我們歸納地定義正負語境（positive context, negative context, strictly positive context） 和 如下，其中 代表一個命題空位（proposition placeholder）：

1. 
2. 如果 ，且 為任意邏輯式，那麼 ， 都屬於 。
3. 如果 ，且 為任意邏輯式，那麼 ， 都屬於 。
4. 
5. 如果 ，那麼 ， 都屬於 。

有限多重集（finite multisets）

多重集中的元素可以重複出現。如果邏輯式 可以從假設的有限多重集 中推導出來，我們記作 ，等同於 。

三大證明體系

• 希爾伯特系統
• 自然演繹（最為常用的版本也是由根岑發明的）
• 相繼式演算（又稱根岑系統）

參考文獻：

Basic proof theory

Handbook of Logic in Computer Science

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

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