编辑“︁Lean经典逻辑”︁

{{DISPLAYTITLE:Lean经典逻辑}}

'''Lean经典逻辑'''是[[Lean定理证明器]]中用于形式化传统数学命题推理的核心系统，基于一阶逻辑和经典命题演算（非构造性逻辑）。与直觉逻辑不同，经典逻辑接受排中律（<math>P \lor \neg P</math>）和双重否定律（<math>\neg \neg P \to P</math>）作为公理，允许通过反证法进行证明。本条目将详细介绍其在Lean 4中的实现、语法及应用。

== 核心概念 ==
经典逻辑在Lean中通过以下关键组件实现：

=== 排中律与反证法 ===
Lean的标准库`Mathlib`提供了经典逻辑的默认支持，关键公理如下：
<syntaxhighlight lang="lean">
-- 排中律（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
</syntaxhighlight>

=== 命题操作符 ===
Lean支持标准逻辑连接词：
* 合取（<code>∧</code>）：`P ∧ Q`
* 析取（<code>∨</code>）：`P ∨ Q`
* 蕴含（<code>→</code>）：`P → Q`
* 否定（<code>¬</code>）：`¬P`
* 等价（<code>↔</code>）：`P ↔ Q`

== 语法与证明策略 ==
以下是经典逻辑中常用的证明策略：

{| class="wikitable"
! 策略 !! 描述 !! 示例
|-
| <code>by_contra</code> || 反证法 || <code>by_contra h</code>
|-
| <code>apply Classical.em</code> || 显式调用排中律 || <code>cases Classical.em P</code>
|-
| <code>push_neg</code> || 否定形式转换 || <code>push_neg at h</code>
|}

=== 示例：德摩根定律 ===
<syntaxhighlight lang="lean">
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
</syntaxhighlight>

== 实际应用案例 ==
=== 案例1：无限集合的性质 ===
证明“自然数集合是无限的”需要经典逻辑：
<syntaxhighlight lang="lean">
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
  -- 后续证明省略...
</syntaxhighlight>

=== 案例2：算法终止性 ===
在证明算法终止性时，经典逻辑可简化非构造性推理：
<syntaxhighlight lang="lean">
def search (p : ℕ → Bool) : ℕ :=
  if h : ∃ n, p n then Classical.choose h else 0
</syntaxhighlight>

== 与直觉逻辑的对比 ==
<mermaid>
flowchart LR
  A[经典逻辑] -->|接受排中律| B[非构造性证明]
  A -->|允许反证法| C[间接存在性]
  D[直觉逻辑] -->|拒绝排中律| E[构造性证明]
  D -->|要求显式构造| F[直接见证]
</mermaid>

== 数学公式支持 ==
经典逻辑的关键定律可用公式表示：
* 排中律：<math>P \lor \neg P</math>
* 双重否定消除：<math>\neg \neg P \implies P</math>
* 逆否命题等价性：<math>(P \implies Q) \iff (\neg Q \implies \neg P)</math>

== 进阶主题 ==
=== 选择公理的关系 ===
Lean中经典逻辑隐含[[选择公理]]的弱形式（通过`Classical.choose`）：
<syntaxhighlight lang="lean">
example (α : Type) (p : α → Prop) : (∃ x, p x) → p (Classical.choose p) :=
  Classical.choose_spec
</syntaxhighlight>

=== 元理论性质 ===
经典逻辑在Lean中的一致性通过以下方式保证：
1. 命题的布尔语义（<math>\llbracket P \rrbracket \in \{0,1\}</math>）
2. 完备性：所有经典重言式在Lean中可证

== 练习建议 ==
1. 形式化证明皮尔士定律：<code>((P → Q) → P) → P</code>
2. 用经典逻辑证明<code>¬¬(P ∨ ¬P)</code>
3. 实现希尔伯特排中律等价形式：<code>P ↔ (¬P → ⊥)</code>

{{提示|在Lean中使用<code>open Classical</code>可自动启用经典推理规则。}}

[[Category:计算机科学]]
[[Category:Lean]]
[[Category:Lean命题逻辑]]