Lean经典逻辑
Lean经典逻辑是Lean定理证明器中用于形式化传统数学命题推理的核心系统，基于一阶逻辑和经典命题演算（非构造性逻辑）。与直觉逻辑不同，经典逻辑接受排中律（）和双重否定律（）作为公理，允许通过反证法进行证明。本条目将详细介绍其在Lean 4中的实现、语法及应用。
核心概念[编辑 | 编辑源代码]
经典逻辑在Lean中通过以下关键组件实现：
排中律与反证法[编辑 | 编辑源代码]
Lean的标准库`Mathlib`提供了经典逻辑的默认支持，关键公理如下：
-- 排中律（Classical.em）
example (P : Prop) : P ∨ ¬P := by
exact Classical.em P
-- 反证法（by_contra）
example (P : Prop) : ¬¬P → P := by
intro h
by_contra hnp
exact h hnp
命题操作符[编辑 | 编辑源代码]
Lean支持标准逻辑连接词：
- 合取（
∧）：`P ∧ Q` - 析取（
∨）：`P ∨ Q` - 蕴含（
→）：`P → Q` - 否定（
¬）：`¬P` - 等价（
↔）：`P ↔ Q`
语法与证明策略[编辑 | 编辑源代码]
以下是经典逻辑中常用的证明策略：
| 策略 | 描述 | 示例 |
|---|---|---|
by_contra |
反证法 | by_contra h
|
apply Classical.em |
显式调用排中律 | cases Classical.em P
|
push_neg |
否定形式转换 | push_neg at h
|
示例：德摩根定律[编辑 | 编辑源代码]
example (P Q : Prop) : ¬(P ∧ Q) ↔ ¬P ∨ ¬Q := by
constructor
· intro h
by_contra hnpq
push_neg at hnpq
exact h ⟨hnpq.1, hnpq.2⟩
· intro h hpq
cases h with
| inl hp => exact hp hpq.1
| inr hq => exact hq hpq.2
实际应用案例[编辑 | 编辑源代码]
案例1：无限集合的性质[编辑 | 编辑源代码]
证明“自然数集合是无限的”需要经典逻辑：
theorem nat_infinite : ¬ ∃ (f : ℕ → ℕ), Function.Bijective f := by
intro ⟨f, hf⟩
have : ∀ n, f n ≥ n := by
intro n
induction n with
| zero => simp
| succ n ih =>
apply Nat.succ_le_of_lt
have := hf.1 (n + 1)
-- 经典逻辑用于排除构造性限制
by_contra h
exact this (Nat.lt_succ_iff.mp h) ih
-- 后续证明省略...
案例2：算法终止性[编辑 | 编辑源代码]
在证明算法终止性时，经典逻辑可简化非构造性推理：
def search (p : ℕ → Bool) : ℕ :=
if h : ∃ n, p n then Classical.choose h else 0
与直觉逻辑的对比[编辑 | 编辑源代码]
数学公式支持[编辑 | 编辑源代码]
经典逻辑的关键定律可用公式表示：
- 排中律：
- 双重否定消除：
- 逆否命题等价性：
进阶主题[编辑 | 编辑源代码]
选择公理的关系[编辑 | 编辑源代码]
Lean中经典逻辑隐含选择公理的弱形式（通过`Classical.choose`）：
example (α : Type) (p : α → Prop) : (∃ x, p x) → p (Classical.choose p) :=
Classical.choose_spec
元理论性质[编辑 | 编辑源代码]
经典逻辑在Lean中的一致性通过以下方式保证： 1. 命题的布尔语义（解析失败 (未知函数“\llbracket”): {\displaystyle \llbracket P \rrbracket \in \{0,1\}} ） 2. 完备性：所有经典重言式在Lean中可证
练习建议[编辑 | 编辑源代码]
1. 形式化证明皮尔士定律：((P → Q) → P) → P
2. 用经典逻辑证明¬¬(P ∨ ¬P)
3. 实现希尔伯特排中律等价形式：P ↔ (¬P → ⊥)