3.1 全稱量詞 forall：對所有人都成立的一句話#

本章導讀#

上一章我們學會了命題邏輯：若則、且、或、非，都是在講固定的句子。這一章要升級了：我們要講「對所有 \(\forall x\) 都成立」的句子。例如「所有自然數加零等於自己」「任意兩數相加可交換」，主詞不再是一個人，而是一整群人。學完這一節，你會用 \(\forall\) 寫規格，用 \(intro\) 引入任意元，用 \(apply\) 把定理套用到具體例子。

淺顯說明#

想像老師說：「全班每位同學都要交作業。」你要怎麼證明這句話？方法是：隨便請一位同學小明上台，但全程不利用「小明是班長」這種特殊身分。如果你對這樣一位「任意同學」都能推出他交了作業，那就等於證明了全班都交了作業。

全稱量詞就是這個意思。 \(\forall x, P(x)\) 讀作「任取一個 \(x\) ，性質 \(P(x)\) 都成立」。在 Lean 裡它就是一個函數：給我任意一個 \(x\) ，我就還你一個 \(P(x)\) 的證明。所以證明全稱命題只有一招：先 \(intro\) 一個任意的 \(x\) ，再證明 \(P(x)\) 。而使用全稱命題也只有一招：把你手上的定理 \(apply\) 到具體的數字或變數上，就像函數呼叫。

初學者常犯兩個錯。第一，把 \(\forall\) 跟大迴圈搞混，以為要在證明裡跑遍所有數，其實只要處理一個「長得很普通」的代表。第二，拿到 \(\forall x, P(x)\) 卻忘記要先餵它一個 \(x\) 才能用，空有食譜卻不買菜。

正規理論#

全稱量詞在依賴型別理論中就是依賴函數型 \(\Pi (x : A), P(x)\) 。即命題 \(\forall x, P(x)\) 的證明，是一個以 \(x\) 為輸入、以 \(P(x)\) 證明為輸出的程式。

\[ \forall x : A, P(x) \;\simeq\; \Pi (x : A), P(x) \]

\[ \frac{\Gamma, x : A \vdash e : P(x)}{\Gamma \vdash fun \; x \Rightarrow e : \forall x, P(x)} \; (\forall I) \qquad \frac{\Gamma \vdash f : \forall x, P(x) \quad \Gamma \vdash a : A}{\Gamma \vdash f \; a : P(a)} \; (\forall E) \]

概念	數學記號	Lean 寫法	說明
全稱命題	\(\forall x, P(x)\)	\(forall \; x, P \; x\)	對一切 \(x\) 成立
依賴函數型	\(\Pi (x : A), P(x)\)	\((x : A) \to P \; x\)	同一概念的型別視角
引入規則	\(\forall I\)	\(intro \; x\)	假設一個任意元
消去規則	\(\forall E\)	\(apply \; h\) 或 \(h \; a\)	實例化到具體的 \(a\)
特例：非依賴	\(A \to P\)	\(A \to P\)	當 \(P\) 不依賴 \(x\) 即退化為蘊涵

引入與消去是一對反操作： \(intro\) 把「任意」包裝起來， \(apply\) 與函數套用把「任意」打開成「具體」。順序不可顛倒：目標是 \(\forall\) 時先 \(intro\) ；假設是 \(\forall\) 時用 \(apply\) 或直接套用。

簡易範例#

目標：陳述加法交換律的一般形式，暫不證明，只練習引入與套用。

-- 陳述：任意兩自然數相加可交換
theorem add_comm_statement (a b : Nat) : a + b = b + a := by
  exact Nat.add_comm a b

-- 練習 intro：把全稱目標剝開
example : ∀ n : Nat, n + 0 = n := by
  intro n
  exact Nat.add_zero n

-- 練習 apply：把已知的全稱定理套到具體數字
example : 3 + 5 = 5 + 3 := by
  apply Nat.add_comm

證明狀態表（第二個例子，目標為 \(\forall n, n + 0 = n\) ）：

步驟	tactic	證明狀態 Goals
起始	—	\(\vdash \forall n : Nat, n + 0 = n\)
1	\(intro \; n\)	\(n : Nat \vdash n + 0 = n\)
2	\(exact \; Nat.add\_zero \; n\)	無剩餘目標，證畢

再看第三個例子。起始目標是 \(3 + 5 = 5 + 3\) ，它沒有 \(\forall\) ，所以不用 \(intro\) 。而 \(Nat.add\_comm\) 的型別是 \(\forall a \; b, a + b = b + a\) ，一句 \(apply \; Nat.add\_comm\) 就讓 Lean 自動把 \(a\) 配對成 \(3\) 、 \(b\) 配對成 \(5\) ，這就是「實例化」。記住口訣：目標有 \(\forall\) 就 \(intro\) ；武器庫有 \(\forall\) 就 \(apply\) 。

歷史典故#

弗雷格《概念文字》：第一次用符號寫出量詞，讓「對一切 \(x\) 」不再只靠日常語言比手畫腳，本節的 \(\forall\) 即源於此。
根岑的自然演繹：把全稱的引入與消去寫成左右對稱的推理規則，Lean 的 \(intro\) 與 \(apply\) 正是這套規則的直接化身。
霍華德的公式即型別：指出 \(\forall\) 就是 \(\Pi\) 型、證明就是函數，本節「給 \(x\) 還證明」的函數視角即由此而來。

習題#

用 \(intro\) 證明 \(\forall n : Nat, n = n\) 。提示：引入 \(n\) 之後只剩 \(n = n\) ，用 \(rfl\) 結束。想一想為何這裡的 \(n\) 必須是「任意」的。
已知 \(Nat.succ\_eq\_add\_one\) 的型別是 \(\forall n, Nat.succ \; n = n + 1\) ，請用 \(apply\) 證明 \(Nat.succ \; 7 = 7 + 1\) 。再試著把 \(7\) 換成變數 \(k\) ，觀察證明有何不同。
試陳述（不必證明）定理： \(\forall a \; b : Nat, a + b = b + a\) 。分別用 \(theorem\) 與 \(example\) 各寫一次，並說明 \(intro \; a\) 之後目標會變成什麼。