逻辑联结词

And/Or/Iff/Exists 的定义、引入与消去规则、经典逻辑公理，以及每个联结词的证明套路。

每个逻辑联结词都是一个归纳类型。掌握它们的引入（怎么造）与消去（怎么用）规则，就掌握了基础证明。

And（∧）

structure And (a b : Prop) : Prop where
  intro ::
  left  : a
  right : b

引入——要造 p ∧ q，给两个证明：

theorem and_intro (p q : Prop) (hp : p) (hq : q) : p ∧ q := ⟨hp, hq⟩

-- tactic 版
theorem and_intro' (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
  constructor
  · exact hp
  · exact hq
-- 或直接
theorem and_intro'' (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
  exact ⟨hp, hq⟩

消去——有 p ∧ q，取出任一边：

theorem and_left (p q : Prop) (h : p ∧ q) : p := h.left      -- 或 h.1
theorem and_right (p q : Prop) (h : p ∧ q) : q := h.right    -- 或 h.2

-- tactic 版：拆开
theorem and_comm' (p q : Prop) (h : p ∧ q) : q ∧ p := by
  obtain ⟨hp, hq⟩ := h
  exact ⟨hq, hp⟩

操作	term	tactic
造	`⟨hp, hq⟩`	`constructor` / `refine ⟨?_, ?_⟩`
拆	`h.1` `h.2`	`obtain ⟨hp, hq⟩ := h` / `cases h`

Or（∨）

inductive Or (a b : Prop) : Prop where
  | inl (h : a) : Or a b
  | inr (h : b) : Or a b

引入——选一边：

theorem or_left (p q : Prop) (hp : p) : p ∨ q := Or.inl hp
theorem or_right (p q : Prop) (hq : q) : p ∨ q := Or.inr hq

-- tactic
theorem or_left' (p q : Prop) (hp : p) : p ∨ q := by
  left
  exact hp

消去——必须两边都处理：

theorem or_comm' (p q : Prop) (h : p ∨ q) : q ∨ p := by
  rcases h with hp | hq
  · right; exact hp
  · left;  exact hq

∧ 与 ∨ 的不对称性：

造 ∧ 要两个证明，用它只需取一个。
造 ∨ 只要一个证明，用它必须处理两种情况。

这个对偶来自它们的构造子数量：And 一个构造子两个字段，Or 两个构造子各一个字段。

Iff（↔）

structure Iff (a b : Prop) : Prop where
  intro ::
  mp  : a → b       -- modus ponens
  mpr : b → a       -- reverse

就是两个方向的蕴含打包：

theorem iff_example (p : Prop) : p ↔ p := ⟨id, id⟩

theorem iff_tactic (p q : Prop) (h1 : p → q) (h2 : q → p) : p ↔ q := by
  constructor
  · exact h1
  · exact h2

用它：

theorem use_iff (p q : Prop) (h : p ↔ q) (hp : p) : q := h.mp hp

Iff 特别有用的地方是可以被 rw 用来重写命题——等价的命题可以互相替换。

Not（¬）与 False

def Not (p : Prop) : Prop := p → False

证否定 = 假设它成立，导出矛盾：

theorem not_example : ¬(1 = 2) := by
  intro h        -- 假设 1 = 2，现在目标是 False
  exact absurd h (by decide)

-- 更简单
theorem not_example' : ¬(1 = 2) := by decide

用否定：

theorem use_not (p : Prop) (hp : p) (hnp : ¬p) : False := hnp hp

hnp hp 就是函数应用——hnp : p → False 作用在 hp : p 上。

全称量词（∀）

theorem forall_example : ∀ n : Nat, n + 0 = n := by
  intro n
  simp

引入用 intro（就是 fun），消去就是应用：

theorem use_forall (h : ∀ n : Nat, n + 0 = n) : 5 + 0 = 5 := h 5

h 5 ——定理当函数用，传入具体值。这正是上一章说的「定理就是函数」。

存在量词（∃）

theorem exists_intro : ∃ n : Nat, n > 5 := ⟨6, by decide⟩

-- tactic 版
theorem exists_intro' : ∃ n : Nat, n > 5 := by
  use 6
  decide

use 提供见证。

消去：

theorem use_exists (h : ∃ n : Nat, n > 5) : ∃ m : Nat, m > 4 := by
  obtain ⟨n, hn⟩ := h
  exact ⟨n, by omega⟩

obtain ⟨n, hn⟩ := h 把存在性拆成「见证 + 性质」。

引入/消去总表

联结词	引入（造）	消去（用）
`p → q`	`intro h` / `fun h => ...`	`h hp`（应用）
`p ∧ q`	`⟨hp, hq⟩` / `constructor`	`h.1` `h.2` / `obtain ⟨_,_⟩`
`p ∨ q`	`left` / `right` / `Or.inl`	`rcases h with h\|h`
`p ↔ q`	`constructor` / `⟨mp, mpr⟩`	`h.mp` `h.mpr` / `rw [h]`
`¬p`	`intro h`（然后证 `False`）	`h hp`（得 `False`）
`∀ x, P x`	`intro x`	`h a`（应用）
`∃ x, P x`	`use a` / `⟨a, ha⟩`	`obtain ⟨x, hx⟩ := h`
`False`	无法引入	`h.elim` / `exact absurd ...`
`True`	`trivial` / `True.intro`	无用

这张表是基础证明的全部工具。看到目标是什么形状，就知道用哪条引入规则；看到假设是什么形状，就知道用哪条消去规则。

经典逻辑

有些命题在构造性逻辑里证不出来：

-- 排中律：需要经典公理
theorem em_example (p : Prop) : p ∨ ¬p := Classical.em p

-- 双重否定消去：同样需要
theorem dne (p : Prop) (h : ¬¬p) : p := Classical.byContradiction fun hn => h hn

Lean 核心是构造性的，但 Mathlib 引入了经典公理（Classical.choice），所以这些都能用。

常用的经典推理 tactic：

theorem by_contra_example (p : Prop) (h : ¬¬p) : p := by
  by_contra hn
  exact h hn

theorem by_cases_example (p q : Prop) (h1 : p → q) (h2 : ¬p → q) : q := by
  by_cases hp : p
  · exact h1 hp
  · exact h2 hp

tactic	作用
`by_contra h`	反证法：假设结论不成立
`by_cases h : p`	分情况：p 成立 / 不成立
`push_neg`	把否定推进量词内部（Mathlib）

push_neg 很实用：

example (P : Nat → Prop) (h : ¬ ∀ n, P n) : ∃ n, ¬ P n := by
  push_neg at h
  exact h

它把 ¬∀ 变成 ∃¬、¬∃ 变成 ∀¬、¬(a < b) 变成 b ≤ a 等等。

想知道一个证明是否用了经典公理：

#print axioms em_example
-- 'em_example' depends on axioms: [Classical.choice, Quot.sound, propext]

纯构造性的证明这里会显示 does not depend on any axioms。

实践中没必要刻意避免经典逻辑——Mathlib 全面使用它。只有做构造性数学或程序提取时才需要在意。

相等（=）

inductive Eq : α → α → Prop where
  | refl (a : α) : Eq a a

只有一个构造子 refl——「每个东西等于它自己」。

这个极简定义蕴含了相等的全部性质：

theorem eq_symm {a b : α} (h : a = b) : b = a := h.symm
theorem eq_trans {a b c : α} (h1 : a = b) (h2 : b = c) : a = c := h1.trans h2
theorem eq_congr {a b : α} (f : α → β) (h : a = b) : f a = f b := congrArg f h

最重要的是替换（Leibniz 律）：

theorem subst_example {a b : α} (P : α → Prop) (h : a = b) (hpa : P a) : P b := h ▸ hpa

▸（\t）读作「用这个等式重写」。tactic 版就是 rw，下一部分详讲。

一个综合练习

theorem demorgan (p q : Prop) : ¬(p ∨ q) ↔ ¬p ∧ ¬q := by
  constructor
  · intro h
    constructor
    · intro hp; exact h (Or.inl hp)
    · intro hq; exact h (Or.inr hq)
  · intro ⟨hnp, hnq⟩ h
    rcases h with hp | hq
    · exact hnp hp
    · exact hnq hq

逐句读：

constructor —— 拆 ↔ 成两个方向。
正向：intro h 拿到 ¬(p ∨ q)，要证 ¬p ∧ ¬q。
再 constructor 拆 ∧，各自 intro 后用 h 配合 Or.inl/Or.inr 造矛盾。
反向：intro ⟨hnp, hnq⟩ h 同时拆开合取并假设 p ∨ q。
rcases 分两种情况，各自用对应的否定得到 False。

这个证明没有任何魔法——全是上面那张表里的引入/消去规则的机械应用。

第 2 部分结束。下一篇进入证明技术：tactic 基础。

本页目录