📐 使用 Lean 4 进行命题逻辑证明：实用指南 🔗

本文将对基础命题逻辑概念及其在 Lean 4 编程语言与定理证明器中的形式化实现进行一次技术梳理。

无论你是希望将证明形式化的数学家，还是深入探索类型论的程序员，本指南都将从第一性原理出发重构逻辑体系。我们将从基本的逻辑常量开始，探索 Lean 4 如何利用柯里-霍华德同构（Curry-Howard Isomorphism）——即命题即类型（propositions are types）、*证明即程序（proofs are programs）*这一核心原则——优雅地对逻辑结构进行建模。

📑 目录 🔗

⚙️ 序言：搭建舞台 🔗

在定义逻辑联结词之前，我们需要先搭建一个基础环境。在 Lean 4 中，这通常通过两个特定命令来完成，以控制作用域和计算行为。

namespace Basic

noncomputable section

• namespace Basic：此命令将我们的定义归入同一个命名空间，防止与 Lean 的内置标准库（Prelude）发生命名冲突。它允许我们出于教学目的，从零开始重新定义 True、False 和 And 等基础结构。
• noncomputable section：Lean 4 既是一个定理证明器，也是一门函数式编程语言。默认情况下，它会尝试为每个定义生成可执行的字节码。将某个部分标记为 noncomputable 会告诉编译器跳过这一步，这在形式逻辑中非常常见，因为在这里我们关心的是数学性质而非运行时执行。

🧩 核心逻辑联结词 🔗

在本节中，我们将定义逻辑的基础元素，将标准数学符号映射为 Lean 4 代码。

✅ 1. 真（True，⊤） 🔗

最简单的命题就是普遍逻辑有效的命题。用编程术语来说，$\top$ 的行为就像一个单元类型（Unit type）——它只有一个状态，且不携带任何额外数据。

定义：

inductive True : Prop where
  | intro : True

因为它仅由单个构造器（intro）定义，所以“证明” True 的唯一方法就是提供这个确切的构造器。

示例：

-- 无条件证明 True
example : True := True.intro

-- 任意命题 'a' 都能平凡地推出 True
example {a : Prop} : a → True := fun _ => True.intro

❌ 2. 假（False，⊥） 🔗

True 是由证明的平凡存在所定义的，而 False 则是通过证明的完全缺失来定义的。它是一个空类型（Empty type 或 Void type）。

定义：

inductive False : Prop

因为 False 没有任何构造器，你永远无法凭空实例化它。它代表逻辑矛盾。

爆炸原理（Principle of Explosion / Ex Falso Quodlibet）： 如果你发现自己手头持有一个 False 的证明，逻辑就会崩塌，你可以由此证明任何事情。Lean 使用递归器（recursor）False.elim 来处理这种情况。

-- 从假命题可以推出任意命题 'a'（⊥ → a）
def False.elim {a : Prop} (false_proof : False) : a := 
  false_proof.rec

🔄 3. 否定（Negation，¬） 🔗

在 Lean 4 中，否定并不是一个原生的内置概念。相反，它是利用蕴涵和 False 以函数方式定义的。要证明命题 $a$ 为假（记作 $\neg a$），你必须展示一个函数：在该函数中，假设 $a$ 成立会直接导出矛盾（$\bot$）。

定义：

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

关键定理：

-- 证明否定：如果假设 'a' 能证明 False，那么 Not 'a' 为真。
theorem Not.intro {a : Prop} (h : a → False) : Not a := 
  fun ha => h ha

-- 双重否定引入（a → ¬¬a）
theorem not_not_intro {a : Prop} (ha : a) : Not (Not a) := 
  fun na => na ha  -- 'na' 的类型为 (a → False)，因此传入 'ha' 会产生 False。

-- 拒取式（Modus Tollens）：如果 (a → b) 且 (¬b)，则 (¬a)
theorem Not.imp {a b : Prop} (nb : Not b) (ab : a → b) : Not a := 
  fun ha => 
    have hb : b := ab ha
    nb hb

➡️ 4. 蕴涵（Implication，→） 🔗

由于 Lean 建立在类型论之上，逻辑蕴涵（$a \to b$）在字面意义上就被当作函数来处理。要证明 $a$ 蕴涵 $b$，你必须编写一个接受任意 $a$ 的证明并返回 $b$ 的证明的函数。

链式蕴涵示例： 如果你能把 $c$ 转化为 $a$，并且能把 $b$ 转化为 $d$，那么你就可以将一个从 $a \to b$ 的函数转化为一个从 $c \to d$ 的函数。

theorem imp_imp_imp {a b c d : Prop} 
  (ca : c → a) (bd : b → d) : (a → b) → (c → d) := 
  fun ab => fun hc => 
    have ha : a := ca hc
    have hb : b := ab ha
    bd hb

🔗 5. 合取（Conjunction，∧） 🔗

逻辑合取要求 $a$ 和 $b$ 同时为真，它在 Lean 中被建模为 structure（结构体）。用编程术语来说，这是一个积类型（Product type，即结构体或元组），同时持有两份独立的证据。

定义：

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

关键证明模式：

-- 引入规则：构造一个 And
example {a b : Prop} (ha : a) (hb : b) : And a b := 
  And.intro ha hb

-- 对称性：a ∧ b → b ∧ a
theorem And.symm {a b : Prop} (h : And a b) : And b a := 
  And.intro h.right h.left

🔀 6. 析取（Disjunction，∨） 🔗

逻辑析取要求两个命题中至少有一个为真。与 And 不同，Or 是一个归纳定义的和类型（Sum type，即带标签联合体），因为存在两种截然不同、二选一的方式来构造其证明。

定义：

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

要证明 $a \lor b$，你可以将 $a$ 的证明包装在 inl（左注入，inject-left）构造器中，或者将 $b$ 的证明包装在 inr（右注入，inject-right）构造器中。

示例：

-- 对称性：a ∨ b → b ∨ a
theorem Or.symm {a b : Prop} (h : Or a b) : Or b a :=
  match h with
  | Or.inl ha => Or.inr ha
  | Or.inr hb => Or.inl hb

↔️ 7. 逻辑等价（Logical Equivalence，↔） 🔗

双向蕴涵，即“当且仅当”（Iff），表示两个命题在逻辑上等价。它被定义为一个同时持有两个方向蕴涵关系的结构体。

定义：

structure Iff (a b : Prop) : Prop where
  intro ::
  mp : a → b
  mpr : b → a

自反性示例：

-- 每个命题都与其自身等价（a ↔ a）
theorem Iff.refl {a : Prop} : Iff a a :=
  Iff.intro (fun ha => ha) (fun ha => ha)

🎯 总结与核心要点 🔗

通过在 Lean 4 中从零开始重建命题逻辑，我们揭示了形式化系统的机械之美：

1. 默认构造主义（Constructive by Default）： 我们定义的是持有真理之证据意味着什么，而不仅仅是断言某件事为真。
2. 命题即类型（Propositions as Types）： 通过柯里-霍华德映射，逻辑联结词直接对应于标准的编程结构：蕴涵是函数，And 是结构体，Or 是枚举，True 是单元类型（unit），而 False 是空类型（void）。
3. 证明即程序（Proofs as Programs）： 在 Lean 中编写数学证明，与编写一个满足特定类型签名的类型安全函数完全等同。

掌握这些基础构建块，将为你攻克更复杂的数学定理、谓词逻辑以及复杂软件系统的形式化验证铺平道路。