跳到主要内容

Lean 命题基础

Lean是一种交互式定理证明器，广泛用于形式化数学和编程语言理论。在Lean中，命题逻辑是构建更复杂证明的基础。本文将介绍Lean中的命题逻辑基础，帮助你理解如何在Lean中定义和证明命题。

什么是命题逻辑？​

命题逻辑是逻辑学的一个分支，研究由命题（即可以判断真假的陈述）组成的逻辑关系。在Lean中，命题通常表示为类型，而证明则是这些类型的项。

命题的定义​

在Lean中，命题可以被视为一种类型。例如，命题 P 可以被定义为：

lean
def P : Prop := true

这里，Prop 是Lean中表示命题的类型，true 是一个简单的命题，表示“真”。

逻辑连接词​

在命题逻辑中，常用的逻辑连接词包括“与”（∧）、“或”（∨）、“非”（¬）和“蕴含”（→）。在Lean中，这些连接词可以通过以下方式定义和使用：

lean
def P : Prop := true
def Q : Prop := false

-- 与
example : P ∧ Q := and.intro P Q

-- 或
example : P ∨ Q := or.inl P

-- 非
example : ¬Q := not.intro (λ h : Q, h)

-- 蕴含
example : P → Q := λ h : P, h

命题的证明​

在Lean中，证明一个命题通常意味着构造一个该命题类型的项。例如，要证明命题 P，我们需要构造一个类型为 P 的项。

lean
def P : Prop := true

-- 证明 P
example : P := trivial

这里，trivial 是Lean中的一个内置证明，用于证明 true 命题。

实际案例​

让我们通过一个实际案例来展示如何在Lean中使用命题逻辑。假设我们有两个命题 P 和 Q，并且我们知道 P 为真，Q 为假。我们希望证明 P ∧ Q 为假。

lean
def P : Prop := true
def Q : Prop := false

-- 证明 P ∧ Q 为假
example : ¬(P ∧ Q) :=
begin
  assume h : P ∧ Q,
  have q : Q := and.right h,
  exact q
end

在这个例子中，我们假设 P ∧ Q 为真，然后通过 and.right 提取出 Q，最后通过 exact q 证明 Q 为假，从而得出矛盾。

总结​

通过本文，我们学习了Lean中命题逻辑的基础知识，包括如何定义命题、使用逻辑连接词以及如何证明命题。这些基础知识是进一步学习Lean和形式化证明的关键。

附加资源​

练习​

  1. 定义两个命题 A 和 B，并证明 A ∨ B。
  2. 尝试证明 ¬(A ∧ ¬A)。
  3. 使用Lean证明 (A → B) → (¬B → ¬A)。

通过这些练习，你将更好地掌握Lean中的命题逻辑基础。