02.3 否定、假與古典邏輯#

本章導讀#

本節收尾命題邏輯，處理最微妙的一組概念：否定與假。

Lean 把否定定義為蘊涵： \(\lnot p\) 就是 \(p \to False\) ，假是無證明的空型別。

你會學會 \(False.elim\) 爆炸原理，以及古典三公理：排中律、選擇與反證法。

最後一張直覺與古典對照表，會告訴你何時該用 \(byContradiction\) 。

否定最直白的讀法是：如果你是對的，世界就爆炸了。

Lean 把爆炸寫成 \(False\) ，一個永遠造不出證據的型別，拿到它就什麼都能證。

所以證否定就是證蘊涵：先假設 \(p\) 成立，再推到矛盾，用 \(intro\) 即可開工。

直覺邏輯只承認這種構造式否定，古典邏輯則多承認排中律：非真即假，沒有中間。

否定的定義只用一行， \(False\) 的消去則是一條公理級規則。

\[ \lnot p := p \to False \]

\[ \frac{\Gamma \vdash False}{\Gamma \vdash p} \quad \text{記為} \; False.elim \]

後者又稱爆炸原理：由矛盾可推出一切，在 Lean 是 \(False.elim\) 。

古典邏輯的三個等價入口如下表，Lean 預設只用前兩行，直覺部分完全構造性。

原理	形式	Lean 名稱	所屬陣營
排中律	\(p \lor \lnot p\)	\(em\) 或 \(Classical.em\)	古典公理
反證法	由 \(\lnot \lnot p\) 得 \(p\)	\(byContradiction\)	古典推論
選擇公理	由全稱存在得選擇函數	\(choice\)	古典公理

三者在古典邏輯中互相等價，其關係可記為：

\[ em \iff \lnot \lnot p \to p \iff choice \]

直覺與古典的差異對照如下，這是本節最重要的總結。

先看純直覺部分：自相矛盾的蘊涵，以及爆炸原理的使用。

theorem not_self_contradiction (p : Prop) : ¬ (p ∧ ¬ p) := by
  intro h
  cases h with
  | intro hp hnp =>
    exact hnp hp

theorem ex_falso (p : Prop) (h : False) : p :=
  False.elim h

古典部分需要排中律，反證法戰術會自動調用它：

theorem dne_classical (p : Prop) (h : ¬¬p) : p := by
  by_contra hc
  exact h hc

證明狀態表以 \(dne\_classical\) 為例，注意 \(by\_contra\) 如何翻轉目標。

步驟	戰術	目標 \(Goals\)	上下文 \(\Gamma\)
初始	無	\(\vdash p\)	\(h : \lnot \lnot p\)
1	\(by\_contra\)	\(\vdash False\)	增加 \(hc : \lnot p\)
2	\(exact\)	\(No goals\)	\(h \; hc : False\) 結案

體會重點： \(byContradiction\) 把要證的 \(p\) 變成要導出矛盾，代價是引入古典公理。

排中律的爭論橫跨兩千年，從哲學一路打到證明器核心。

Lean 的立場是務實的：預設構造性，需要時再用 \(Classical\) 開啟古典模式。