Lean命题基础

Lean命题基础

Lean命题基础是学习Lean定理证明器的核心起点，它涵盖了命题逻辑的基本构造、语法规则和证明方法。本节将系统介绍如何在Lean中表示和操作命题，包括逻辑联结词、真值、以及简单证明的构建方式。

命题逻辑简介

命题逻辑（Propositional Logic）是数学逻辑的基础分支，研究由原子命题（不可再分的陈述句）通过逻辑联结词（如∧、∨、→、¬）组合而成的复合命题。在Lean中，命题被表示为类型，其证明则是该类型的项。

核心概念

• 命题：可判断真假的陈述（如"2是偶数"）。
• 真值：命题的取值（True/False）。
• 逻辑联结词：

 * 合取（$\wedge$）：`P ∧ Q`
 * 析取（$\vee$）：`P ∨ Q`
 * 蕴含（$\to$）：`P → Q`
 * 否定（$\mathrm{\neg }$）：`¬P`

Lean中的命题表示

在Lean中，命题是`Prop`类型的对象。以下示例展示如何声明命题并使用联结词：

-- 声明两个命题变量
variables (P Q : Prop)

-- 复合命题示例
#check P ∧ Q      -- 合取
#check P ∨ Q      -- 析取
#check P → Q      -- 蕴含
#check ¬P         -- 否定

输出： ``` P ∧ Q : Prop P ∨ Q : Prop P → Q : Prop ¬P : Prop </syntaxhighlight>

基本证明方法

Lean使用构造性逻辑，证明即给出对应命题的具体构造。以下是常见命题的证明示例：

合取证明

example (hP : P) (hQ : Q) : P ∧ Q :=
⟨hP, hQ⟩  -- 使用尖括号构造合取证明

析取证明

example (hP : P) : P ∨ Q :=
or.inl hP  -- 选择左分支证明

蕴含证明

example : P → P :=
λ hP => hP  -- 使用lambda表达式处理假设

真值表与逻辑等价

通过真值表可验证命题的等价性。例如解析失败 (语法错误): {\displaystyle P → Q} 等价于$\mathrm{\neg }P\vee Q$：

flowchart LR A[P] -->|true| B[Q] A -->|false| C[¬P ∨ Q = true]

数学表示： $P\to Q\equiv \mathrm{\neg }P\vee Q$

实际案例：登录系统验证

假设需要验证一个登录系统的逻辑规则："如果用户已认证且令牌有效，则允许访问"。用Lean表示为：

variables (authenticated valid_token : Prop)
theorem access_rule (h1 : authenticated) (h2 : valid_token) : access_granted :=
⟨h1, h2⟩  -- 构造合取证明

常见错误与调试

1. 类型不匹配：确保所有子命题类型为`Prop`

   -- 错误示例
   example (n : Nat) : n → n := λ x => x  -- Nat不是命题！

2. 未消解假设：所有假设必须被使用

   -- 错误示例
   example (hP : P) : Q := sorry  -- 未使用hP

进阶概念

• 经典逻辑：通过`open Classical`使用排中律
• 命题等价性：用`↔`表示双向蕴含

  example : P ∧ Q ↔ Q ∧ P :=
  ⟨λ h => ⟨h.right, h.left⟩, λ h => ⟨h.right, h.left⟩⟩

练习

尝试证明以下命题：

example : P → ¬¬P :=
λ hP => λ hnP => hnP hP

提示：否定¬P在Lean中定义为`P → False`。