编辑“︁Lean逻辑连接词”︁

{{DISPLAYTITLE:Lean逻辑连接词}}

'''逻辑连接词'''是命题逻辑中的基本构建块，用于组合简单命题形成复杂命题。在Lean定理证明器中，逻辑连接词是形式化数学和编程验证的核心工具。本文将全面介绍Lean中五种主要逻辑连接词：合取（∧）、析取（∨）、蕴含（→）、否定（¬）和等价（↔）。

== 逻辑连接词概述 ==
在Lean中，逻辑连接词被定义为'''归纳类型'''或'''常量'''，其行为遵循构造演算的规则。以下是基础连接词的类型签名：

<math>\begin{align*}
&\wedge\ :\ Prop\ \to\ Prop\ \to\ Prop \\
&\vee\ :\ Prop\ \to\ Prop\ \to\ Prop \\
&\to\ :\ Prop\ \to\ Prop\ \to\ Prop \\
&\neg\ :\ Prop\ \to\ Prop \\
&\leftrightarrow\ :\ Prop\ \to\ Prop\ \to\ Prop
\end{align*}</math>

== 合取（Conjunction, ∧）==
合取表示"且"关系，要求两个命题同时为真。

=== 语法与构造 ===
<syntaxhighlight lang="lean">
-- 构造合取命题
example : 2 + 2 = 4 ∧ 3 + 3 = 6 := 
  ⟨by norm_num, by norm_num⟩
</syntaxhighlight>

输出结果：
<pre>⊢ 2 + 2 = 4 ∧ 3 + 3 = 6</pre>

=== 分解使用 ===
<syntaxhighlight lang="lean">
example (h : p ∧ q) : p := h.left
example (h : p ∧ q) : q := h.right
</syntaxhighlight>

== 析取（Disjunction, ∨）==
析取表示"或"关系，至少一个命题为真即可。

=== 基本用法 ===
<syntaxhighlight lang="lean">
-- 从左构造析取
example : 2 + 2 = 4 ∨ 1 = 0 := Or.inl (by norm_num)
-- 从右构造析取
example : 1 = 0 ∨ 3 = 3 := Or.inr (by norm_num)
</syntaxhighlight>

=== 案例分析 ===
<mermaid>
graph TD
    A[假设 p ∨ q] --> B[情况拆分]
    B --> C[子证明 p → r]
    B --> D[子证明 q → r]
    C --> E[得到 r]
    D --> E
</mermaid>

== 蕴含（Implication, →）==
蕴含表示"如果...那么..."关系，是Lean中最常用的连接词。

=== 函数对应 ===
在Curry-Howard同构下，蕴含对应函数类型：
<syntaxhighlight lang="lean">
example (h : p → q) (hp : p) : q := h hp
</syntaxhighlight>

=== 证明策略 ===
使用<code>intro</code>策略处理假设：
<syntaxhighlight lang="lean">
example : p → p := by
  intro h
  exact h
</syntaxhighlight>

== 否定（Negation, ¬）==
否定实际上是蕴含的特殊形式：<math>\neg p \equiv p \to \text{False}</math>

=== 典型证明 ===
<syntaxhighlight lang="lean">
example (h : p ∧ ¬p) : False := h.right h.left
</syntaxhighlight>

== 等价（Equivalence, ↔）==
等价是双向蕴含，定义为合取两个方向的蕴含。

=== 构造示例 ===
<syntaxhighlight lang="lean">
example : p ↔ p := 
  ⟨fun h => h, fun h => h⟩
</syntaxhighlight>

== 优先级规则 ==
Lean中逻辑连接词的优先级（从高到低）：
# ¬
# ∧, ∨
# →
# ↔

== 实际应用案例 ==
'''软件规范验证'''：验证排序算法的前后条件
<syntaxhighlight lang="lean">
theorem sort_correct (arr : Array α) :
  (is_sorted (sort arr)) ∧ (arr.toList.Perm (sort arr).toList) := by
  apply And.intro
  · -- 证明排序后有序
  · -- 证明结果是排列
</syntaxhighlight>

== 练习建议 ==
1. 证明交换律：<code>p ∧ q ↔ q ∧ p</code>
2. 构造德摩根定律：<code>¬(p ∨ q) ↔ ¬p ∧ ¬q</code>
3. 实现蕴含传递性：<code>(p → q) → (q → r) → (p → r)</code>

== 高级主题 ==
对于有经验的用户，可以探讨：
* 连接词的计算行为差异
* 经典逻辑与直觉主义逻辑的区别
* 连接词在依赖类型中的扩展应用

通过掌握这些逻辑连接词，用户将能够构建复杂的逻辑陈述并在Lean中进行形式化验证。

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