2.2 量詞：∀ 與 ∃#

本節目標#

理解全稱量詞 \(\forall\) 與存在量詞 \(\exists\) 的數學意義。
學會 Lean 的四大核心 tactic：intro（面對 ∀）、exact/apply（使用 ∀）、use（證明 ∃）、obtain（使用 ∃）。
練習嵌套量詞的結構化證明，例如 \(\forall \varepsilon > 0,\ \exists \delta > 0\) 。
認識量詞順序顛倒造成的常見錯誤。

數學意義#

全稱量詞 \(\forall x \in S,\ P(x)\) 意思是「對 \(S\) 中每一個 \(x\) ， \(P(x)\) 都成立」。證明它的標準方法是：任取一個 \(x\) （不設任何條件），然後證明 \(P(x)\) 。使用它的方法則是：代入具體的值，例如由 \(\forall n,\ P(n)\) 得到 \(P(3)\) 。

存在量詞 \(\exists x \in S,\ P(x)\) 意思是「 \(S\) 中至少有一個 \(x\) 使 \(P(x)\) 成立」。證明它的標準方法是：指出一個具體的例子（witness）。使用它的方法則是：得到某個滿足性質的 \(x\) ，但通常不知道它是誰。

量詞	證明（建構）	使用（消去）
\(\forall\)	任取 \(x\) ，證 \(P(x)\)	代入具體值
\(\exists\)	給出 witness \(a\) 與證據 \(P(a)\)	拿到 witness 與證據

對應到 Lean tactic：

Lean 目標 / 證據	tactic
目標 `∀ x, P x`	`intro x`
目標 `∃ x, P x`	`use a`
證據 `h : ∀ x, P x`	`exact h a` 或 `apply h`
證據 `h : ∃ x, P x`	`obtain ⟨x, hx⟩ := h`

∀ 的證明與使用#

在 Curry–Howard 的觀點下，∀ x, P x 是一個函數型別：給它一個 \(x\) ，它就回傳 \(P\ x\) 的證明。所以 intro 就是「接收參數」：

-- 對所有自然數 n，n + 0 = n（這其實是 Mathlib 的 Nat.add_zero）
example (n : Nat) : n + 0 = n := Nat.add_zero n

-- intro 的基本用法
example : ∀ n : Nat, n = n := by
  intro n
  rfl

-- ∀ 可以有多層參數，intro 逐一接收
example : ∀ a b : Nat, a + b = b + a := by
  intro a b
  rw [Nat.add_comm]

-- 使用 ∀：當函數呼叫
example (P : Nat → Prop) (h : ∀ n, P n) : P 3 := by
  exact h 3

∃ 的證明與使用#

證明 ∃ x, P x 用 use：先給出 witness，再證明它滿足性質。使用 ∃ 用 obtain：把 witness 和證據一起解構出來。

-- 存在一個自然數的平方等於 4
example : ∃ n : Nat, n * n = 4 := by
  use 2
  rfl

-- 存在偶質數
example : ∃ p : Nat, p > 1 ∧ p < 3 := by
  use 2
  norm_num

-- 使用 ∃：obtain 解構出 witness 與證據
example (h : ∃ n : Nat, n * n = 4) : ∃ n : Nat, n = 2 ∨ n = 2 := by
  obtain ⟨n, hn⟩ := h
  use n
  left
  exact hn

obtain ⟨x, hx⟩ := h 中，x 是 witness、hx : P x 是證據。這在數學證明的白話就是「設 \(x\) 為那個存在的元素，則我們知道 \(P(x)\) 」。

嵌套量詞： \(\forall \varepsilon > 0,\ \exists \delta > 0\)#

這是分析學中最核心的句型。考慮簡化版的連續性：函數 \(f(x) = x\) 在 \(0\) 處「連續」—— 對任意 \(\varepsilon > 0\) ，存在 \(\delta > 0\) ，使 \(|x| < \delta \Rightarrow |x| < \varepsilon\) 。取 \(\delta = \varepsilon\) 即可。Lean 版本：

example : ∀ ε : ℝ, ε > 0 → ∀ x : ℝ, |x| < ε → |x| < ε := by
  intro ε hε x hx
  exact hx

-- 真正的挑戰：對 ε > 0 找 δ > 0，使得 |x| < δ ⇒ |2x| < ε
-- 策略：取 δ = ε / 2
example : ∀ ε : ℝ, ε > 0 → ∃ δ : ℝ, δ > 0 ∧ ∀ x, |x| < δ → |2 * x| < ε := by
  intro ε hε
  use ε / 2
  constructor
  · positivity
  · intro x hx
    rw [abs_mul]
    simp only [abs_of_pos (two_pos : (2 : ℝ) > 0), two_mul]
    rw [abs_lt] at hx ⊢
    constructor
    · linarith
    · linarith

注意證明的骨架就是量詞的順序：

intro ε hε —— 面對最外層的 \(\forall \varepsilon\) 。
use ε / 2 —— 面對 \(\exists \delta\) ，交出 witness。
constructor —— 拆出「 \(\delta > 0\) 」與「 \(\forall x, \ldots\) 」兩個子目標。
intro x hx —— 面對內層的 \(\forall x\) ，同時收到假設 \(|x| < \delta\) 。
用 rw / linarith 等化簡工具收尾。

原則：目標長什麼樣，就 intro 什麼；遇到 ∃，就 use 一個精心挑選的式子。

使用 ∀ 的進階技巧：`apply` 與特化#

當目標是 P 5 而手上有一個 h : ∀ n, P n，exact h 5 直接特化；當形狀不完全吻合時，apply 會讓 Lean 嘗試反推需要代入的值：

example (P : Nat → Nat → Prop) (h : ∀ a b, P a b) : P 1 2 := by
  apply h

常見錯誤：量詞順序顛倒#

\[ \forall x \in \mathbb{R},\ \exists y \in \mathbb{R},\ y > x \]

是真的（取 \(y = x + 1\) ）。但

\[ \exists y \in \mathbb{R},\ \forall x \in \mathbb{R},\ y > x \]

是假的：沒有一個實數比所有實數都大。順序一換，真理就翻轉。在 Lean 中看得一清二楚：

-- ∀∃ 版本：可證
example : ∀ x : ℝ, ∃ y : ℝ, y > x := by
  intro x
  use x + 1
  linarith

-- ∃∀ 版本：不可證！以下的證明骨架會失敗——
-- use 之後馬上要對「所有 x」證明，而我們固定的 y 太弱了
-- example : ∃ y : ℝ, ∀ x : ℝ, y > x := by
--   intro y   -- 錯：還不能 intro，得先 use

另一個直觀例子：

「每個人都有一個母親」： \(\forall x\, \exists m,\ \text{母}(m, x)\) —— 真。
「有一個人是所有人的母親」： \(\exists m\, \forall x,\ \text{母}(m, x)\) —— 假。

記憶法：誰在外層誰先 intro；∃ 的 witness 只能依賴它左邊（外層）的變數。 ∀ ε, ∃ δ 中 δ 可以依賴 ε（這正是連續性！）；∃ δ, ∀ ε 中 δ 不能依賴 ε（這會強到變成一致性連續甚至常數函數）。

小結與練習#

重點回顧：

∀ 證明用 intro，使用用 h x 或 apply。
∃ 證明用 use，使用用 obtain ⟨x, hx⟩。
嵌套量詞按順序處理：外層 ∀ 先 intro，中間 ∃ 用 use，內層繼續 intro。
量詞順序不可交換； \(\forall\varepsilon\,\exists\delta\) 與 \(\exists\delta\,\forall\varepsilon\) 天差地遠。

練習（依難度分級）：

基礎

證明：∀ n : Nat, 0 + n = n（提示：Nat.zero_add）。
證明：∃ n : Nat, n ^ 2 = 25。
證明：∃ n : Nat, n > 100 ∧ n < 102。

進階

證明：∀ x : ℝ, ∃ y : ℝ, y * y > x（提示：分 \(x < 0\) 與 \(x \geq 0\) ，或取 \(y = x + 1\) 用 nlinarith）。
證明：對任意 \(\varepsilon > 0\) ，存在 \(n \in \mathbb{N}\) 使 \(1/n < \varepsilon\) （Archimedean 性質，提示：exists_nat_gt）。
證明 \(f(x) = x^2\) 在 \(0\) 處連續的雛形： ∀ ε > 0, ∃ δ > 0, ∀ x, |x| < δ → x * x < ε（取 \(\delta = \sqrt{\varepsilon}\) ，提示：use Real.sqrt ε 與 Real.lt_sqrt、Real.sqrt_pos）。

挑戰

證明 ¬ ∃ y : ℝ, ∀ x : ℝ, y > x（提示：intro + push_neg 或 intro ⟨y, hy⟩ 後取 x := y 導出矛盾）。
證明：∀ ε > 0, ∃ δ > 0, ∀ x, |x| < δ → |x ^ 3| < ε（提示：取 \(\delta = \min(1, \varepsilon)\) ，當 \(|x| \leq 1\) 時 \(|x|^3 \leq |x|\) ；需要用到 min_lt_min、abs_pow 與 nlinarith 或 pow_le_one）。