Lean矛盾证明

Lean矛盾证明

Lean矛盾证明（Proof by Contradiction in Lean）是命题逻辑中一种重要的证明方法，其核心思想是通过假设命题的否定成立，推导出矛盾，从而证明原命题为真。在Lean定理证明器中，这种方法常用于处理复杂的逻辑命题，尤其适用于无法直接构造证明的情况。

介绍

在逻辑学中，矛盾证明（又称反证法）的基本步骤如下： 1. 假设命题$P$不成立（即假设$\mathrm{\neg }P$为真）。 2. 从$\mathrm{\neg }P$出发，推导出一个矛盾（例如$Q\wedge \mathrm{\neg }Q$）。 3. 由此得出结论：假设$\mathrm{\neg }P$不成立，因此$P$必须为真。

在Lean中，这种证明方法通过`by_contra`或`by_contradiction`策略实现，适用于构造性逻辑无法直接证明的命题。

基本语法与示例

以下是一个简单的Lean代码示例，展示如何使用矛盾证明：

example (P : Prop) : ¬¬P → P :=
begin
  intro hnnp,              -- 假设¬¬P成立
  by_contra hnp,           -- 假设¬P成立（目标变为推导出矛盾）
  apply hnnp hnp,          -- 应用¬¬P到¬P，得到矛盾
end

输出效果：该证明表明，在经典逻辑中，双重否定律$\mathrm{\neg }\mathrm{\neg }P\to P$成立。通过假设$\mathrm{\neg }P$并推导出矛盾（即$\mathrm{\neg }\mathrm{\neg }P$与$\mathrm{\neg }P$冲突），证明了$P$必须为真。

详细步骤解析

1. 假设阶段：通过`intro hnnp`引入假设$\mathrm{\neg }\mathrm{\neg }P$。 2. 矛盾假设：`by_contra hnp`声明要使用矛盾证明，并假设$\mathrm{\neg }P$。 3. 推导矛盾：`apply hnnp hnp`将$\mathrm{\neg }\mathrm{\neg }P$应用于$\mathrm{\neg }P$，生成矛盾（因为$\mathrm{\neg }\mathrm{\neg }P$等价于“$\mathrm{\neg }P$会导致矛盾”）。 4. 结论：Lean自动识别矛盾，完成证明。

实际应用案例

案例1：证明无理数的存在

以下代码证明$\sqrt{2}$是无理数：

theorem sqrt_two_irrational : ¬∃ (m n : ℕ), m.coprime n ∧ m^2 = 2 * n^2 :=
begin
  by_contradiction h,      -- 假设存在这样的m和n
  rcases h with ⟨m, n, h_coprime, h_eq⟩,
  have : 2 ∣ m,            -- 推导出2整除m
  { sorry },               -- 此处省略具体推导
  have : 2 ∣ n,            -- 进一步推导出2整除n
  { sorry },
  have : ¬m.coprime n,     -- 与互质假设矛盾
  { sorry },
  contradiction            -- 显式声明矛盾
end

案例2：逻辑命题的否定

证明命题$P\to Q$的否定等价于$P\wedge \mathrm{\neg }Q$：

example (P Q : Prop) : ¬(P → Q) ↔ (P ∧ ¬Q) :=
begin
  split,
  { intro h,
    by_contra h',          -- 假设¬(P ∧ ¬Q)
    apply h,               -- 推导矛盾
    intro hp,
    by_contra hnq,
    exact h' ⟨hp, hnq⟩ },  -- 构造P ∧ ¬Q引发矛盾
  { sorry }                -- 反向证明省略
end

矛盾证明的局限性

在构造性逻辑中，矛盾证明的某些形式（如双重否定律）不被接受。Lean默认支持经典逻辑，但可以通过以下方式显式声明：

open classical

可视化逻辑流程

graph TD A[假设¬P] --> B[推导出Q] A --> C[推导出¬Q] B & C --> D[矛盾] D --> E[结论P成立]

数学公式支持

矛盾证明的数学表述： $\begin{array}{rl}& \text{若}\mathrm{\neg }P⊢\mathrm{\perp },\text{则}⊢P\\ & \text{其中}\mathrm{\perp }\text{表示矛盾}\end{array}$

总结

• 适用场景：当直接证明困难时，或需处理否定命题时。
• 核心策略：`by_contra`或`by_contradiction`。
• 注意事项：在构造性逻辑中需谨慎使用。

通过矛盾证明，Lean用户可以高效处理复杂的逻辑关系，尤其在经典数学证明中具有显著优势。