Lean 直觉主义逻辑

介绍

直觉主义逻辑（Intuitionistic Logic）是一种与经典逻辑不同的逻辑体系，它强调数学构造和证明的“构造性”。与经典逻辑不同，直觉主义逻辑不接受排中律（即“命题A或非A”不一定成立），除非能够明确构造出A的证明或非A的证明。Lean作为一种交互式定理证明器，支持直觉主义逻辑，并提供了丰富的工具来探索这一领域。

在本教程中，我们将逐步介绍Lean中的直觉主义逻辑，并通过代码示例和实际案例帮助你理解其核心概念和应用。

直觉主义逻辑与经典逻辑的区别

在经典逻辑中，排中律（Law of Excluded Middle）是一个基本原则，即对于任何命题A，A ∨ ¬A总是成立。然而，在直觉主义逻辑中，排中律并不被接受，除非我们能够明确构造出A的证明或¬A的证明。

例如，在经典逻辑中，我们可以通过反证法证明某些命题，而在直觉主义逻辑中，这种证明方法可能不被接受，因为它依赖于排中律。

备注

经典逻辑 vs 直觉主义逻辑

经典逻辑：接受排中律，允许非构造性证明。
直觉主义逻辑：拒绝排中律，强调构造性证明。

Lean 中的直觉主义逻辑

Lean默认使用直觉主义逻辑，这意味着在Lean中，所有的证明都必须是构造性的。让我们通过一个简单的例子来理解这一点。

示例：构造性证明

假设我们有一个命题 P : Prop，我们希望证明 P ∨ ¬P。在经典逻辑中，这总是成立的，但在直觉主义逻辑中，我们需要明确构造出 P 的证明或 ¬P 的证明。

lean
example (P : Prop) : P ∨ ¬P :=
begin
  -- 这里无法直接证明，因为我们需要构造性的证明
  sorry
end

在Lean中，上述代码会报错，因为我们无法直接构造出 P ∨ ¬P 的证明。相反，我们需要提供具体的构造性证明。

实际案例：直觉主义逻辑的应用

案例1：构造性存在证明

假设我们有一个类型 α 和一个谓词 P : α → Prop，我们希望证明存在某个 x : α 使得 P x 成立。在直觉主义逻辑中，我们需要明确构造出这样的 x。

lean
example (α : Type) (P : α → Prop) : (∃ x : α, P x) → (∃ x : α, P x) :=
begin
  intro h,
  cases h with x hx,
  exact ⟨x, hx⟩,
end

在这个例子中，我们通过 cases 分解了存在量词，并明确构造出了满足条件的 x。

案例2：拒绝排中律

在直觉主义逻辑中，我们不能直接使用排中律。例如，以下代码会报错：

lean
example (P : Prop) : P ∨ ¬P :=
begin
  -- 这里无法直接证明
  sorry
end

如果我们希望使用排中律，我们需要明确假设它：

lean
open classical

example (P : Prop) : P ∨ ¬P :=
begin
  exact em P,
end

在这里，我们通过 open classical 引入了经典逻辑的假设，从而可以使用排中律。

总结

直觉主义逻辑强调构造性证明，拒绝非构造性的方法，如排中律。在Lean中，默认使用直觉主义逻辑，因此所有的证明都必须是构造性的。通过本教程，你已经了解了直觉主义逻辑的核心概念，并通过代码示例和实际案例掌握了其应用。

附加资源与练习

附加资源

Lean官方文档
《类型论与函数式编程》——深入了解构造性逻辑与类型论的关系。

练习

尝试在Lean中证明 ¬¬(P ∨ ¬P)，并解释为什么这个命题在直觉主义逻辑中成立。
构造一个存在性证明，证明存在一个自然数 n 使得 n + 1 = 2。

通过完成这些练习，你将进一步巩固对Lean直觉主义逻辑的理解。

介绍​

直觉主义逻辑与经典逻辑的区别​

Lean 中的直觉主义逻辑​

示例：构造性证明​

实际案例：直觉主义逻辑的应用​

案例1：构造性存在证明​

案例2：拒绝排中律​

总结​

附加资源与练习​

附加资源​

练习​

介绍