Lean 逻辑连接词
在Lean中，逻辑连接词是构建命题逻辑的基础工具。它们允许我们将简单的命题组合成更复杂的命题。本文将详细介绍Lean中的逻辑连接词，包括合取（∧）、析取（∨）、蕴含（→）和否定（¬），并通过代码示例和实际案例帮助你理解它们的用法。
1. 逻辑连接词简介
逻辑连接词是用于连接命题的符号或词语，它们定义了命题之间的关系。在Lean中，逻辑连接词是形式化数学和逻辑推理的核心工具。以下是Lean中常用的逻辑连接词：
- 合取（∧）：表示“与”，只有当两个命题都为真时，合取命题才为真。
- 析取（∨）：表示“或”，只要有一个命题为真，析取命题就为真。
- 蕴含（→）：表示“如果...那么...”，只有当前提为真而结论为假时，蕴含命题才为假。
- 否定（¬）：表示“非”，用于否定一个命题的真值。
2. 合取（∧）
合取连接词用于表示两个命题同时为真的情况。在Lean中，合取符号为 ∧。
代码示例
example : true ∧ true :=
begin
split,
{ exact true.intro },
{ exact true.intro }
end
在这个例子中，我们证明了 true ∧ true 为真。split 策略将合取命题分解为两个子目标，分别证明 true 和 true。
实际应用
假设我们有两个命题 P 和 Q，我们希望证明 P ∧ Q。我们可以使用 split 策略将目标分解为 P 和 Q，然后分别证明它们。
3. 析取（∨）
析取连接词用于表示两个命题中至少有一个为真的情况。在Lean中，析取符号为 ∨。
代码示例
example : true ∨ false :=
begin
left,
exact true.intro
end
在这个例子中，我们证明了 true ∨ false 为真。left 策略选择了左边的命题 true 进行证明。
实际应用
假设我们有两个命题 P 和 Q，我们希望证明 P ∨ Q。我们可以使用 left 或 right 策略选择其中一个命题进行证明。
4. 蕴含（→）
蕴含连接词用于表示“如果...那么...”的关系。在Lean中，蕴含符号为 →。
代码示例
example : true → true :=
begin
intro h,
exact true.intro
end
在这个例子中，我们证明了 true → true。intro 策略引入了前提 h : true，然后我们证明了结论 true。
实际应用
假设我们有一个命题 P 和 Q，我们希望证明 P → Q。我们可以使用 intro 策略引入前提 P，然后证明 Q。
5. 否定（¬）
否定连接词用于表示一个命题的相反情况。在Lean中，否定符号为 ¬。
代码示例
example : ¬false :=
begin
intro h,
exact h
end
在这个例子中，我们证明了 ¬false。intro 策略引入了假设 h : false，然后我们通过 h 得出矛盾。
实际应用
假设我们有一个命题 P，我们希望证明 ¬P。我们可以使用 intro 策略引入假设 P，然后通过逻辑推理得出矛盾。
6. 实际案例
让我们通过一个实际案例来综合运用这些逻辑连接词。假设我们有以下命题：
P：今天下雨。Q：我带伞。
我们希望证明以下命题：
- 如果今天下雨，那么我带伞。
- 今天下雨且我带伞。
- 今天不下雨或我带伞。
代码示例
variables (P Q : Prop)
example : P → Q :=
begin
intro h,
-- 在这里证明 Q
end
example : P ∧ Q :=
begin
split,
{ -- 在这里证明 P },
{ -- 在这里证明 Q }
end
example : ¬P ∨ Q :=
begin
-- 在这里证明 ¬P 或 Q
end
在这个案例中，我们展示了如何使用逻辑连接词来构建和证明复杂的命题。
7. 总结
逻辑连接词是Lean中构建命题逻辑的基础工具。通过合取、析取、蕴含和否定，我们可以将简单的命题组合成更复杂的命题，并通过逻辑推理来证明它们的真值。希望本文能帮助你理解这些逻辑连接词的基本概念和用法。
8. 附加资源与练习
- 练习1：尝试证明
P ∨ ¬P（排中律）。 - 练习2：尝试证明
(P → Q) → (¬Q → ¬P)（逆否命题）。 - 附加资源：阅读Lean官方文档中关于逻辑连接词的更多内容。
通过不断练习和探索，你将更加熟练地掌握Lean中的逻辑连接词，并能够运用它们解决更复杂的逻辑问题。