1934 年：Gentzen 自然演繹 — 證明的結構重建#

偵探：Gerhard Gentzen（Hilbert 弟子）。案發地：哥廷根。卷宗：自然演繹＋矢列演算＋切消定理。

案發現場#

1931-Godel不完備定理.md 炸毀了 Hilbert（1900-Hilbert23問題.md）的一致性美夢，1910-PrincipiaMathematica.md 與 1879-Frege概念文字.md 的希爾伯特式公理證明又冗長到反人類：連 \(A ∧ B ⊢ A\) 都要繞經三公理。

Gentzen 接到的報案是雙重的：能否讓證明像自然推理一樣書寫？能否讓證明有可分析的結構，從而挽回一致性證明？

他的回答是自然演繹（Natural Deduction）與矢列演算（Sequent Calculus）LK/LJ，外加皇冠上的切消定理（Hauptsatz）。

自然演繹每式為 \(Γ ⊢ A\) ，每個連結詞各有一對引入（I）消去（E）規則：

示例：證 \(A ∧ B ⊢ B ∧ A\) 只需兩次 \(∧\) 消去加一次 \(∧\) 引入，三步收工——希爾伯特式要十數步。

\[ \frac{A ∧ B}{B} ∧ E \quad \frac{A ∧ B}{A} ∧ E \]

\[ \frac{B \quad A}{B ∧ A} ∧ I \]

矢列形如 \(Γ ⇒ Δ\) ，讀作「 \(Γ\) 合取蘊涵 \(Δ\) 析取」。結構規則＋邏輯規則分離：

古典 LK 右側可多公式，直覺 LJ 右側至多一公式——一字之差劃開古典與構造性世界，後世證明助手的理論分水嶺。

Hauptsatz：一切切皆可消去。任何用引理（切）的證明都可展開為無切的直接證明：

\[ \frac{Γ ⇒ A \quad A ⇒ Δ}{Γ ⇒ Δ} Cut \leadsto \text{無切證明} \]

推論有三：子公式性質（證明只含結論的子公式）、一致性（空矢列 \(⇒\) 證不出，故系統一致）、插值定理。

自然演繹側對應正規化：消去「引入緊接消去」的繞路（detour），如 \(→I\) 後接 \(→E\) 即 \(β\) 化簡。Gentzen 藉此（加超限歸納到 \(ε_0\) ）證明了算術一致性——對 1931-Godel不完備定理.md 的部分救贖：有窮不行，超限可以。

Gentzen 結案：證明有了結構理論。推理不再是公理的盲目堆疊，而是引入/消去的對稱舞蹈，切消即計算。

遺產：

第一幕在此落幕：從 -0350-Aristotle三段論.md 的分類，到 1847-Boole布林代數.md 的計算、1879-Frege概念文字.md 的語言、1900-Hilbert23問題.md 的夢想、1910-PrincipiaMathematica.md 的 attempt、1929-Herbrand定理.md 的機械化、1931-Godel不完備定理.md 的極限，終於在 Gentzen 手中長出可計算、可分析的證明結構。

核心矢列：

\[ A ∧ B ⇒ B ∧ A \]

\[ Γ ⇒ A, Δ \quad Γ, A ⇒ Δ \text{ 之切可消} \]

最小 Python 演示正規化即求值（ \(→I/E\) 對應 \(λ\) /apply）：

# (λx. x + 1)(41) -> 42：引入緊接消去 = 繞路，化簡即計算
term = (lambda x: x + 1)(41)
assert term == 42
print("detour eliminated:", term)