跳轉到

3.2 存在量詞 exists：拿出一個見證人#

本章導讀#

上一節講「全部都成立」，這一節講相反的：「至少有一個成立」。 例如「存在一個偶數」「存在一組 \(x\) 讓方程式有解」，只要拿出一個例子就算贏。 學完這一節，你會用 \(use\) 親手交出見證人，用 \(cases\) 把別人交出來的包裹拆開，理解 \(\exists\) 背後的 \(\Sigma\) 型。

淺顯說明#

想像有人質疑：「世界上真的有會發光的魚嗎？」 你不用解釋全海洋的魚，只要從口袋掏出一條鮟鱇魚放在桌上，全場安靜。 這條魚就叫「見證人」。存在性證明就是變出見證人的魔術。

在 Lean 裡， \(\exists x, P(x)\) 是一個包裹，裡面裝了兩樣東西：一個具體的 \(w\) ，加上一張證明書 \(P(w)\) 。 證明存在命題用 \(use\) ：例如要證 \(\exists n, n \% 2 = 0\) ，一句 \(use \; 4\) 就把見證人定為 \(4\) ，剩下證明 \(4 \% 2 = 0\) 。 使用存在假設用 \(cases\) 或 \(obtain\) ：把包裹拆成「有個 \(w\) 」加上「它滿足性質」，再繼續推理。 千萬別把存在跟全稱搞反： \(use\) 是「我來選數字」， \(intro\) 是「別人任意給數字」。

正規理論#

存在量詞對應依賴對型 \(\Sigma (x : A), P(x)\) ，即一個值與一個證明的配對。

\[ \exists x : A, P(x) \;\simeq\; \Sigma (x : A), P(x) \]
\[ \frac{\Gamma \vdash a : A \quad \Gamma \vdash h : P(a)}{\Gamma \vdash \langle a, h \rangle : \exists x, P(x)} \; (\exists I) \qquad \frac{\Gamma \vdash e : \exists x, P(x) \quad \Gamma, x : A, h : P(x) \vdash c : C}{\Gamma \vdash match \; e : C} \; (\exists E) \]
概念 數學記號 Lean 寫法 說明
存在命題 \(\exists x, P(x)\) \(Exists \; x, P \; x\) 至少一個 \(x\) 使 \(P(x)\) 成立
見證對 \(\langle w, h \rangle\) \(\langle w, h \rangle\) 見證人加證明書的配對
引入規則 \(\exists I\) \(use \; w\) 交出見證人 \(w\)
消去規則 \(\exists E\) $cases \; h \; with \; \; intro \; w \; hw$
偶數定義 \(Even(n) := \exists k, n = 2 * k\) \(Even \; n\) 本節範例的核心謂詞

注意構造性含義： \(\exists\) 的證明必須真的算出見證人，不能只說「應該有」。 這正是 \(\Sigma\) 型的精神：沒有見證人的存在性是空頭支票。

簡易範例#

目標：證明存在偶數，並練習從存在假設中取出見證人。

-- 例一：4 是偶數的見證人
example : ∃ n : Nat, Even n := by
  use 4
  decide

-- 例二：承上，偶數加二仍是偶數（拆包裹再包裝）
example (h : ∃ n : Nat, Even n) : ∃ m : Nat, Even m := by
  cases h with
  | intro w hw =>
    use w + 2
    omega

證明狀態表（例一，目標為 \(\exists n, Even \; n\) ）：

步驟 tactic 證明狀態 Goals
起始 — \(\vdash \exists n : Nat, Even \; n\)
1 \(use \; 4\) \(\vdash Even \; 4\)
2 \(decide\) 無剩餘目標，證畢

例二的狀態變化也值得看：起始只有一個假設 \(h : \exists n, Even \; n\) 。 一句 \(cases \; h\) 之後，上下文多出 \(w : Nat\) 與 \(hw : Even \; w\) ，目標不變。 這時我們選新見證人 \(w + 2\) ，再交給 \(omega\) 收尾。 口訣：要證 \(\exists\) 就 \(use\) ；手上有 \(\exists\) 就 \(cases\) 。

歷史典故#

  • 弗雷格《概念文字》：同時發明 \(\forall\) 與 \(\exists\) ，讓「存在一個 \(x\) 」第一次有了嚴格符號，本節的見證人思想即奠基於此。
  • 羅賓遜的歸結原理：把存在量詞經 Skolem 化變成可計算的見證函數，自動定理證明從此能機械地「變出見證人」。
  • Prolog 邏輯程式：把 \(\exists x, P(x)\) 的證明變成查詢求解， \(use\) 交見證正好對應 Prolog 回答「 \(x = 4\) 」的瞬間。

習題#

  1. 證明 \(\exists n : Nat, n \% 2 = 0\) 。提示：選 \(use \; 6\) 或 \(use \; 10\) ，再用 \(decide\) 或 \(rfl\) 收尾。換一個見證人再證一次。
  2. 假設 \(h : \exists k : Nat, n = 2 * k\) ，請用 \(cases \; h\) 拆出 \(k\) 與等式，並說明拆完後上下文多了哪兩行。試著改用 \(obtain \; \langle k, hk \rangle := h\) 寫法。
  3. 證明：若 \(\exists n, Even \; n\) ，則 \(\exists m, Even \; (m + 2)\) 。提示：先拆包裹得 \(w\) ，再用 \(use \; (w + 2)\) 。思考為何不能直接 \(use \; w\) 結束。