编辑“︁Lean谓词逻辑”︁（章节）

= Lean谓词逻辑 =

'''Lean谓词逻辑'''（Predicate Logic in Lean）是命题逻辑的扩展，它允许对个体、变量、量词（全称量词∀和存在量词∃）以及谓词（描述个体性质的函数）进行形式化推理。在Lean定理证明器中，谓词逻辑是构建数学证明和形式化验证的核心工具之一。

== 简介 ==

谓词逻辑在Lean中通过内置的逻辑框架和类型系统实现。与命题逻辑仅处理简单命题不同，谓词逻辑可以表达更复杂的陈述，例如“对于所有自然数''n''，''n + 0 = n''”或“存在一个实数''x''，使得''x² = 2''”。Lean的谓词逻辑支持以下关键特性：
* '''个体变量'''：表示特定域（如自然数、集合等）中的对象。
* '''谓词'''：接受一个或多个参数并返回命题的函数（如`Even(n)`表示“''n''是偶数”）。
* '''量词'''：`∀`（全称量词）和`∃`（存在量词）用于量化变量。

== 基本语法与示例 ==

=== 全称量词（∀） ===
在Lean中，全称量词`∀`表示“对于所有”。以下是一个简单示例：
<syntaxhighlight lang="lean">
example : ∀ (n : ℕ), n + 0 = n :=
fun n => Nat.add_zero n
</syntaxhighlight>
'''解释'''：
* `∀ (n : ℕ)`声明了一个自然数变量`n`。
* `n + 0 = n`是待证明的命题。
* `fun n => Nat.add_zero n`是一个匿名函数（λ表达式），它使用Lean的标准库定理`Nat.add_zero`完成证明。

=== 存在量词（∃） ===
存在量词`∃`表示“存在至少一个”。示例：
<syntaxhighlight lang="lean">
example : ∃ (n : ℕ), n > 0 :=
Exists.intro 1 (Nat.zero_lt_one)
</syntaxhighlight>
'''解释'''：
* `∃ (n : ℕ), n > 0`声明存在一个自然数`n`使得`n > 0`。
* `Exists.intro 1`提供见证`1`，并调用`Nat.zero_lt_one`证明`1 > 0`。

== 谓词的定义与使用 ==

谓词是返回命题的函数。例如，定义一个“偶数”谓词：
<syntaxhighlight lang="lean">
def Even (n : ℕ) : Prop := ∃ (k : ℕ), n = 2 * k

example : Even 4 :=
Exists.intro 2 (by simp)
</syntaxhighlight>
'''解释'''：
* `Even`谓词定义为“存在`k`使得`n = 2 * k`”。
* 证明`Even 4`时，提供`k = 2`并通过`simp`策略简化计算。

== 量词的嵌套与交互 ==

谓词逻辑允许量词嵌套。例如：
<syntaxhighlight lang="lean">
example : ∀ (n : ℕ), ∃ (m : ℕ), m > n :=
fun n => Exists.intro (n + 1) (Nat.lt_succ_self n)
</syntaxhighlight>
'''解释'''：
* 对于任意自然数`n`，存在`m = n + 1`使得`m > n`。
* `Nat.lt_succ_self n`是Lean标准库中`n < n + 1`的证明。

== 实际应用案例 ==

=== 数学定理形式化 ===
形式化数学陈述“任意两个连续自然数中至少有一个是偶数”：
<syntaxhighlight lang="lean">
theorem consecutive_evens : ∀ (n : ℕ), Even n ∨ Even (n + 1) :=
fun n => Or.elim (Nat.even_or_odd n)
  (fun h => Or.inl h)
  (fun h => Or.inr (h ▸ Even (n + 1)))
</syntaxhighlight>
'''步骤'''：
1. 使用`Nat.even_or_odd`将`n`分为偶数或奇数情况。
2. 若`n`为偶数，直接得证（`Or.inl`）。
3. 若`n`为奇数，则`n + 1`为偶数（通过`h ▸`替换）。

=== 程序验证 ===
验证列表操作的正确性：
<syntaxhighlight lang="lean">
def NonEmpty (α : Type) (lst : List α) : Prop := ∃ (x : α), x ∈ lst

example : NonEmpty ℕ [1, 2, 3] :=
Exists.intro 1 (by simp)
</syntaxhighlight>
'''解释'''：
* `NonEmpty`谓词断言列表非空。
* 提供见证`1`并通过`simp`策略证明`1 ∈ [1, 2, 3]`。

== 图表辅助理解 ==

<mermaid>
graph LR
  A[谓词逻辑] --> B[全称量词 ∀]
  A --> C[存在量词 ∃]
  A --> D[谓词]
  B --> E["∀x, P(x)"]
  C --> F["∃x, P(x)"]
  D --> G["P(x): x 的性质"]
</mermaid>

== 数学公式支持 ==

在谓词逻辑中，公式可能涉及嵌套量词，例如：
<math>
\forall x \, (\text{Even}(x) \to \exists y \, (x = 2 \times y))
</math>

== 总结 ==
Lean的谓词逻辑为形式化数学和程序验证提供了强大工具。通过量词、谓词和依赖类型系统的结合，用户可以精确表达和证明复杂命题。初学者应从简单例子入手，逐步掌握量词推理和谓词定义。

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