跳到主要内容

Lean 矛盾证明

介绍​

在命题逻辑中，矛盾证明法（Proof by Contradiction）是一种常用的推理方法。它的核心思想是：假设命题的否定为真，然后通过逻辑推理得出矛盾，从而证明原命题为真。这种方法在Lean中同样适用，并且是形式化验证的重要工具之一。

本文将逐步讲解如何在Lean中使用矛盾证明法，并通过代码示例和实际案例帮助你理解这一概念。

什么是矛盾证明法？​

矛盾证明法的基本步骤如下：

  1. 假设命题 P 的否定 ¬P 为真。
  2. 通过逻辑推理，从 ¬P 推导出一个矛盾（例如 Q ∧ ¬Q）。
  3. 由于假设 ¬P 导致了矛盾，因此原命题 P 必须为真。

在Lean中，我们可以使用 by_contra 策略来实现这一过程。

在Lean中使用矛盾证明法​

基本语法​

在Lean中，by_contra 是一个用于矛盾证明的策略。它的语法如下：

lean
by_contra h

其中，h 是假设命题的否定。接下来，我们需要在假设 h 的基础上推导出矛盾。

示例1：证明 ¬¬P → P​

让我们从一个简单的例子开始：证明双重否定蕴含原命题，即 ¬¬P → P。

lean
example (P : Prop) : ¬¬P → P :=
begin
  intro h,          -- 假设 ¬¬P
  by_contra hnp,    -- 假设 ¬P
  apply h,          -- 应用 ¬¬P
  exact hnp,        -- 得出矛盾
end

解释：

  1. intro h：假设 ¬¬P 为真。
  2. by_contra hnp：假设 ¬P 为真。
  3. apply h：将 ¬¬P 应用于 ¬P，得到 P。
  4. exact hnp：由于 P 和 ¬P 同时成立，产生矛盾。

示例2：证明 P ∨ ¬P​

接下来，我们证明排中律 P ∨ ¬P。这是一个经典逻辑中的命题，但在直觉逻辑中并不成立。

lean
example (P : Prop) : P ∨ ¬P :=
begin
  by_contra h,      -- 假设 ¬(P ∨ ¬P)
  apply h,          -- 应用假设
  right,            -- 选择 ¬P
  intro hp,         -- 假设 P
  apply h,          -- 应用假设
  left,             -- 选择 P
  exact hp,         -- 得出矛盾
end

解释：

  1. by_contra h：假设 ¬(P ∨ ¬P) 为真。
  2. apply h：将假设应用于 P ∨ ¬P。
  3. right：选择 ¬P。
  4. intro hp：假设 P 为真。
  5. apply h：再次应用假设。
  6. left：选择 P。
  7. exact hp：得出矛盾。

实际案例​

案例1：证明 ¬(P ∧ ¬P)​

这是一个经典命题，表示“命题 P 和其否定 ¬P 不能同时为真”。

lean
example (P : Prop) : ¬(P ∧ ¬P) :=
begin
  intro h,          -- 假设 P ∧ ¬P
  cases h with hp hnp,  -- 分解假设
  apply hnp,        -- 应用 ¬P
  exact hp,         -- 得出矛盾
end

解释：

  1. intro h：假设 P ∧ ¬P 为真。
  2. cases h with hp hnp：将假设分解为 P 和 ¬P。
  3. apply hnp：应用 ¬P。
  4. exact hp：得出矛盾。

案例2：证明 ¬(P ↔ ¬P)​

这个命题表示“命题 P 不能等价于其否定 ¬P”。

lean
example (P : Prop) : ¬(P ↔ ¬P) :=
begin
  intro h,          -- 假设 P ↔ ¬P
  cases h with h1 h2,  -- 分解假设
  by_cases p : P,   -- 对 P 进行分情况讨论
  { apply h1,       -- 应用 P → ¬P
    exact p,        -- 得出 ¬P
    exact p },      -- 得出矛盾
  { apply h2,       -- 应用 ¬P → P
    exact p,        -- 得出 P
    exact p }       -- 得出矛盾
end

解释：

  1. intro h：假设 P ↔ ¬P 为真。
  2. cases h with h1 h2：将假设分解为 P → ¬P 和 ¬P → P。
  3. by_cases p : P：对 P 进行分情况讨论。
  4. 在每种情况下，通过应用假设得出矛盾。

总结​

矛盾证明法是命题逻辑中一种强大的推理工具，尤其在形式化验证中非常有用。通过假设命题的否定并推导出矛盾，我们可以有效地证明原命题为真。

在Lean中，by_contra 策略是实现矛盾证明法的关键。通过本文的示例和案例，你应该能够掌握如何在Lean中使用这一方法。

附加资源与练习​

练习​

  1. 证明 ¬(P → Q) → P ∧ ¬Q。
  2. 证明 ¬(P ∨ Q) → ¬P ∧ ¬Q。
  3. 尝试用矛盾证明法证明 ¬(P ∧ Q) → ¬P ∨ ¬Q。

进一步学习​

  • 阅读Lean官方文档中关于命题逻辑的部分。
  • 尝试在Lean中实现其他经典逻辑命题的证明。
提示

如果你在练习中遇到困难，可以尝试分解命题并逐步推理。矛盾证明法需要一定的练习才能熟练掌握！