# 逻辑联结词

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

- 作者：David（道雾轩）
- 专栏：Lean 4 从入门到精通（https://daiw.org/manual/lean4.md）
- 最后更新：2026-08-02
- 原文：https://daiw.org/manual/lean4/logic-connectives
- 转载与引用：请注明出处并附原文链接（https://daiw.org/about/copyright）

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

## And（∧）

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

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

```lean
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`，取出任一边：

```lean
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（∨）

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

**引入**——选一边：

```lean
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
```

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

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

<Callout type="info">
  **`∧` 与 `∨` 的不对称性**：

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

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

## Iff（↔）

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

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

```lean
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
```

用它：

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

`Iff` 特别有用的地方是可以被 [`rw`](https://daiw.org/manual/lean4/rewriting) 用来重写命题——等价的命题可以互相替换。

## Not（¬）与 False

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

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

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

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

用否定：

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

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

## 全称量词（∀）

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

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

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

`h 5` ——定理当函数用，传入具体值。这正是[上一章](https://daiw.org/manual/lean4/propositions-as-types)说的「定理就是函数」。

## 存在量词（∃）

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

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

`use` 提供见证。

消去：

```lean
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` | 无用 |

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

## 经典逻辑

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

```lean
-- 排中律：需要经典公理
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：

```lean
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` 很实用：

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

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

<Callout type="info">
  想知道一个证明是否用了经典公理：

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

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

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

## 相等（=）

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

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

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

```lean
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 律）：

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

`▸`（`\t`）读作「用这个等式重写」。tactic 版就是 [`rw`](https://daiw.org/manual/lean4/rewriting)，下一部分详讲。

## 一个综合练习

```lean
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
```

逐句读：

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

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

第 2 部分结束。下一篇进入证明技术：[tactic 基础](https://daiw.org/manual/lean4/tactics-basics)。