2.4 反證法與逆否命題#

本節目標#

• 理解反證法（proof by contradiction）與逆否命題（contrapositive）的數學意義。
• 學會 Lean tactic：by_contra、push_neg、by_cases。
• 認識經典邏輯（Classical）與直覺主義邏輯的差異：排中律的角色。
• 熟悉 not_not、absurd、Classical.byContradiction 等常用引理。

數學意義#

反證法：想證 \(P\) ，就先假設 \(\lnot P\) ，推出矛盾（False）， 於是 \(\lnot P\) 不可能成立，故 \(P\) 成立。

這條規則叫做雙重否定消去。它看起來無害，卻是「經典邏輯」的標誌—— 直覺主義邏輯不接受它（見後文淺談）。

逆否命題： \(P \to Q\) 與 \(\lnot Q \to \lnot P\) 等價。 證明 \(\lnot Q \to \lnot P\) 有時比直接證 \(P \to Q\) 容易， 因為「 \(\lnot Q\) 成立」是額外的資訊，可以用來推導。

經典例子： \(\sqrt{2}\) 是無理數（預告）#

標準證明是反證法：假設 \(\sqrt{2} = a/b\) （最簡分數），推導出 \(a, b\) 同為偶數， 矛盾。Mathlib 中已有此定理，摘錄其敘述：

-- Mathlib 已證明：√2 是無理數
-- #check @irrational_sqrt_two
-- irrational_sqrt_two : Irrational √2

完整形式化頗長（需要良序原理、無窮遞降等工具），本節先練習它的「骨架」： 如何假設矛盾、如何使用 ¬ 型的假設。

by_contra：反證法入門#

by_contra h 把目標 \(P\) 變成假設 h : ¬P，然後目標變成 False：

example (p : Prop) (h : ¬¬p) : p := by
  by_contra hp
  exact h hp

-- 一行的 term mode：Classical.byContradiction
example (p : Prop) (h : ¬¬p) : p := Classical.byContradiction h

注意：這個 by_contra 能證的，直覺主義也承認一半—— by_contra 本質上呼叫 Classical.byContradiction，所以用了它就進入經典邏輯。 Lean 的建構主義核心不內建雙重否定消去，必須明確引入 Classical 命名空間的工具。

push_neg：把否定推過量詞與連接詞#

push_neg 把「否定」往裡推，換成等價的規範形式：

example (p q : Prop) (h : ¬(p ∧ q)) : ¬p ∨ ¬q := by
  push_neg at h  -- h 變成 ¬p ∨ ¬q
  exact h

-- 否定全稱量詞：¬∀ 變 ∃¬
example (P : Nat → Prop) (h : ¬∀ n, P n) : ∃ n, ¬P n := by
  push_neg at h
  exact h

更嚴謹的示範：

example (P : Nat → Prop) (h : ∃ n, ¬P n) : ¬∀ n, P n := by
  intro hall       -- 目標 False；hall : ∀ n, P n
  obtain ⟨n, hn⟩ := h
  exact hn (hall n)

example (P : Nat → Prop) (h : ¬∃ n, P n) : ∀ n, ¬P n := by
  intro n hn
  exact h ⟨n, hn⟩

-- push_neg 的正向用途：證明不等式時把 ¬a ≤ b 化為 a > b
example (a b : ℝ) (h : ¬(a ≤ b)) : b < a := by
  push_neg at h
  exact h

by_cases：排中律的二分法#

\(P \lor \lnot P\) 是排中律（law of excluded middle）。在經典邏輯中永遠可用， by_cases hp : p 會產生兩個分支：hp : p 與 hp : ¬p：

example (p q : Prop) (h : (p → q) → p) : p := by
  by_cases hp : p
  · exact hp
  · -- 假設 ¬p：則 p → q 對任何 q 成立（爆炸原理），套 h 得 p，矛盾
    exact absurd (h (fun hp' => absurd hp' hp)) hp

-- 排中律本身在 Lean 中必須來自 Classical：
#check @Classical.em
-- Classical.em : ∀ (p : Prop), p ∨ ¬p

by_cases 與 Classical.em 是同一件事的 tactic 化。 直覺主義者會說：知道 \(\lnot\lnot P\) 並不真的「建構出」 \(P\) 的證據； 但排中律讓我們可以「先假定不在，看會發生什麼」——這是反證法與二分討論的共同基礎。

直覺主義 vs 經典邏輯（淺談）#

直覺主義拒絕排中律的理由：若 \(P\) 是「存在一個反例」，用排中律「證」 \(P\) 等於沒有真的找出那個例子。在 Curry–Howard 下，直覺主義的證明就是可執行程式， 所以每個 \(\exists\) 證明都附帶一個可以計算的 witness。 Lean 選了務實路線：核心是直覺主義的，但透過 Classical 公理層提供完整經典邏輯。 所以你可以自由使用 by_contra、by_cases，只是要記得它們是「加料」的工具。

常用引理一覽（都在 Classical 或 Not 附近）：

#check @Classical.em            -- p ∨ ¬p
#check @Classical.byContradiction -- ¬¬p → p
#check @not_not                 -- ¬¬p ↔ p
#check @absurd                  -- a → ¬a → b
#check @not_forall              -- ¬∀ x, p x ↔ ∃ x, ¬p x（需 Classical）

綜合範例：逆否命題證法#

定理：若 \(x^2 = 0\) 則 \(x = 0\) 的逆否版本——若 \(x \neq 0\) 則 \(x^2 \neq 0\) ：

example (x : ℝ) (hx : x ≠ 0) : x ^ 2 ≠ 0 := by
  intro h        -- 假設 x^2 = 0
  exact hx (pow_eq_zero_iff (by norm_num) |>.mp h)

-- 反證法版本
example (x : ℝ) : x ^ 2 = 0 → x = 0 := by
  intro h
  by_contra hx
  have hx' : x ≠ 0 := hx
  exact hx' (pow_eq_zero_iff (by norm_num) |>.mp h)

第一個證明是直接的逆否推理（其實就是普通蘊含）； 第二個是反證法。觀察：反證法版本繞了一圈卻也完成了任務—— 很多時候，反證法能讓「否定條件」變成可用的正面資訊（例如 \(x \neq 0\) 拿來當除法分母非零的依據），這正是它的價值。

小結與練習#

重點回顧：

• 反證法：by_contra h 假設 \(\lnot P\) 推矛盾；背後是 Classical.byContradiction。
• push_neg 把否定規範化： \(\lnot\forall \to \exists\lnot\) 、 \(\lnot(a \leq b) \to a > b\) 。
• by_cases = 排中律二分法 = Classical.em。
• 直覺主義核心不收雙重否定消去；Classical 公理層補上經典邏輯。
• 逆否命題 \(\lnot Q \to \lnot P\) 與 \(P \to Q\) 等價（此等價本身在直覺主義下單向成立）。

練習（依難度分級）：

基礎

1. 用 by_contra 證明：¬¬True → True。
2. 證明：(x : ℕ) → x ≠ 0 → x + 1 ≠ 0（用 intro 與 Nat.succ_ne_zero，不需反證法）。
3. 用 push_neg 證明：(a b : ℝ) → ¬(a < b) → b ≤ a。

進階

1. 證明：¬∃ n : ℕ, n + 1 = 0（提示：intro ⟨n, hn⟩ 後 omega 或 exact Nat.succ_ne_zero n hn.symm）。
2. 用 by_cases 證明：(p : Prop) → (p ∨ ¬p) → (¬¬p → p)。
3. 證明：(P Q : Prop) → (¬Q → ¬P) → (P → Q)（逆否命題；需要 by_cases 分討論）。

挑戰

1. 挑戰平方根骨架：在 Lean 中證明「不存在有理數 \(r\) 使 \(r^2 = 2\) 」的關鍵引理： 若 \(a^2 = 2b^2\) （ \(a, b : ℕ\) ），則 \(a\) 是偶數（提示：Nat.abs 不需要， 用 Nat 的奇偶性引理 Nat.even_or_odd 與平方的奇偶性）。
2. 證明：(∀ P : Prop, P ∨ ¬P) → (¬¬p → p)——從排中律推導雙重否定消去， 並說明為什麼反向（從雙否消去推排中律）在直覺主義下也需要額外步驟 （提示：對 \(p \lor \lnot p\) 取雙重否定後用 De Morgan）。