3.3 命題即型別、證明即項：Curry–Howard 在 Lean 中的實體化#

本節目標#

理解 Curry–Howard 對應在 Lean 中的具體形態：theorem 也是定義
掌握 Prop 的 impredicativity 與 proof irrelevance 的意義與用途
區分 definitional equality 與 propositional equality
認識 Lean 的三大公理（propext、Classical.choice、Quot.sound）與 #print axioms

Curry–Howard：邏輯就是程式#

Curry–Howard 對應（又稱 proofs-as-programs）說的是一件事：直覺主義邏輯的證明與 \(\lambda\) 演算的程式是同一個東西的兩種讀法。公式即型別，證明即程式，證明化簡即程式求值。

Lean 把這個對應實體化到極致——在 Lean 的 kernel 眼中，根本沒有「定理」與「函數」的區別：

-- 一個普通的定義
def double (n : Nat) : Nat := n + n

-- 一個「定理」：語法上多一個修飾詞，本質上是一樣的
theorem two_lt_four : 2 < 4 := Nat.lt_succ_self 3

-- 用 #print 看看 theorem 的「內容」：
#print two_lt_four
-- 輸出：theorem two_lt_four : 2 < 4 := fun x => x.succ.pred ...（proof term）

theorem 與 def 的唯一差別是：

	`def`	`theorem`
回傳型別	任意（通常在 `Type`）	必在 `Prop`
內容可否 `#print` / 展开	可以	kernel 層級 proof irrelevance 使其無意義（可看 proof term，但不參與計算）
能否被計算使用	能	否（`Prop` 不能 eliminate 到 `Type`）

定理的「值」是一個 proof term——一個型別為某命題的項。2 < 4 這個命題的證明，就是一個型別為 2 < 4 的程式。沒有第二種真理的來源：要證明一個命題，就是要在 Lean 語言裡寫出一個型別正確的項，並讓 kernel 驗收。

一個 proof term 長什麼樣#

以交換律為例，先看 tactic 版本：

theorem and_comm' (p q : Prop) : p ∧ q → q ∧ p := by
  intro ⟨hp, hq⟩
  exact ⟨hq, hp⟩

再寫出它的 proof term 版本（兩者 kernel 收到的東西一模一樣）：

theorem and_comm'' (p q : Prop) : p ∧ q → q ∧ p :=
  fun h : p ∧ q =>
    And.intro (And.right h) (And.left h)

讀法：p ∧ q 的型別（即 And p q）是積型別，它的項是配對 ⟨hp, hq⟩；蘊含 → 是 \(\Pi\) 型別，它的項是 fun。and_comm'' 本身就是一個普通的依值函數——只不過它的回傳型別落在 Prop。

更進一步，連「前提」也可以用 \(\Pi\) 寫進型別：

-- modus ponens，作為一個項：
theorem mp (p q : Prop) (h : p → q) (hp : p) : q := h hp
-- proof term: fun p q h hp => h hp
-- 型別: ∀ (p q : Prop), (p → q) → p → q
-- 這就是 Hilbert 系統的公理 K 與 S 可以被構造的原因

`Prop` 的 impredicativity 與 proof irrelevance#

3.2 節說過 Prop = Sort 0 是 impredicative 的。這帶來兩個重要後果：

後果一：小的命題宇宙。 量化整個 Prop 得到的仍是 Prop，不會升層級。這讓二階邏輯的命題（如 Peano 的歸納公理「對所有性質 \(P\) ……」）可以寫在一個層級內。

後果二：proof irrelevance（證明無關性）。 這是一條 kernel 規則：

-- 任何兩個型別相同的證明都是相等的
theorem proof_irrel {p : Prop} (h₁ h₂ : p) : h₁ = h₂ := proofIrrel h₁ h₂

意思：命題只在乎是否可證，不在乎用哪個證明。2 < 4 的兩個證明，不管多複雜多笨，在 kernel 眼中都是同一個。這在數學哲學上是 Propo sitional logic 的立場（命題的真假才是重點），在工程上則是巨大簡化——kernel 檢查證明時不必比對證明的「形狀」。

對比之下，Type 層級的資料是 proof relevant 的：兩個不同的 List Nat 當然不同，內容就是意義。

兩種相等：definitional vs propositional#

Lean 中「相等」有兩層，初學者最容易混淆：

Definitional equality（定義相等 / 判斷相等）：kernel 可以純粹用計算判定的相等。包括 \(\beta\) 化約、 \(\delta\) （展開定義）、 \(\iota\) （recursor 化約）。判定是可決定的、機械的。

-- 這些都是 definitional equality，kernel 自動判定，不需證明
example : (fun x => x + 1) 3 = 4 := rfl        -- β 化約
example : Nat.succ (Nat.succ Nat.zero) = 2 := rfl

Propositional equality（命題相等）：需要給出證明的相等。它是一條命題（落在 Prop），要用 Eq 的證明項來建立。

-- 這不是 definitional equality，需要真正證明
theorem two_plus_two : 2 + 2 = 4 := rfl  -- 碰巧這個是 definitional
-- 但加法交換律不是：
theorem add_comm_nat (n m : Nat) : n + m = m + n := Nat.add_comm n m

判斷的經驗法則：kernel 願意用 rfl（reflect，定義相等）收下的，是 definitional；需要 tactic 或顯式項的，是 propositional。 兩者的界線取決於定義寫法，這也是為什麼 mathlib 對「效能友善的定義」很講究——定義寫得好，更多等式變成 definitional，simp 與 decide 就能自動處理。

Lean 的三大公理#

Lean 的 kernel 本身幾乎不需要公理——CIC 的規則（ \(\Pi\) 、 \(\Sigma\) 、歸納型別、recursor）都是構造性的。但為了古典數學的方便，標準庫加入了三條公理：

#print axioms Classical.em
-- 'Classical.em' depends on axioms: [propext, Classical.choice, Quot.sound]

公理	內容	作用
`propext`	若兩命題互為推論，則它們相等	讓 `simp` 可以「同義替換」命題
`Classical.choice`	非空型別存在一個選擇函數	古典邏輯：排中律、雙重否定消除
`Quot.sound`	商型別的良構性	構造有理數、實數等商結構

三個關鍵觀察：

只有三條，而且都是宇宙級的結構公理，不是數學公理。Peano 公理、歸納法、選擇公理以外的所有數學，都由歸納型別與定義構造出來。
Classical.choice 是唯一的非構造性公理，而且被限制在 Prop 層級使用（Classical.choice : {α : Sort u} → Nonempty α → α，實際上落回 Sort u，但配合 proof irrelevance 使用安全）。Lean 用型別系統把非構造性「關進籠子」。
Quot.sound 是構造實數的必需品——實數是 Cauchy 序列的商，商需要等價關係的良構性。

換句話說：Lean 形式化數學時，數學公理本身就是定義或定理。Peano 的歸納公理？Nat.rec 自帶。實分析？由 Quot + 定義構造。這是「數學不需要額外公理」的精確含義：邏輯框架（CIC）+ 三條結構公理，足以構造目前數學界使用的全部主流數學。

用 `#print axioms` 替證明做「血統檢驗」#

這個指令在大型數學庫的工程化中出奇地有用：

-- 一個只用構造性方法證明的定理
theorem constructed_example : 2 + 2 = 4 := rfl
#print axioms constructed_example
-- 'constructed_example' does not depend on any axioms

-- 一個用了古典邏輯的定理
theorem classical_example (p : Prop) : p ∨ ¬p := Classical.em p
#print axioms classical_example
-- depends on axioms: [propext, Classical.choice]

mathlib 的審核者會用 #print axioms 檢查新定理的血統：一個標榜構造性的定理如果依賴 Classical.choice，就是錯誤分類。在 AI 時代這更有意思——當證明由神經網路生成時，#print axioms 是驗證其邏輯純度的最後防線。

小結與練習#

本節重點：

Curry–Howard 在 Lean 中是實體規則：定理就是定義，證明就是型別正確的項
Prop impredicative + proof irrelevance，使命題只在乎可證性
Definitional equality 由 kernel 計算判定；propositional equality 需要證明
Lean 只有三大公理：propext、Classical.choice、Quot.sound，其餘數學皆為構造
#print axioms 是檢驗證明血統的工程工具

練習：

寫出 theorem or_comm (p q : Prop) : p ∨ q → q ∨ p 的純項版本（不用 by），然後用 #print 對照
用 #print axioms 檢查以下定理各依賴哪些公理：Nat.add_comm、Nat.le_trans、Classical.byContradiction
構造一個 definitional equality 成立但乍看不像的例子（提示：Nat.add 的定義方向），說明為什麼 rfl 能收下
思考題：proof irrelevance 說「證明的形狀不重要」，但證明採礦（proof mining）卻能從證明中提取演算法。這兩者矛盾嗎？查閱 proof mining 的相關文獻後回答。