Lean中简单蕴含证明疑问：如何表达命题p不成立的情况？

首先要明确：Lean这类定理证明器采用的是构造逻辑，而非纯经典逻辑的真值表解释，这是理解“证明即程序”对应关系的核心。

1. p → p的构造性解释 #

你写出的fun x => x完全贴合构造逻辑中蕴含的定义：

• 命题p → p对应函数类型p → p（这里的p既是命题也是类型，它的元素就是p的证明）。
• 函数fun x => x的含义是：若给我一个p的证明x，我就能返回x作为p的证明——完美实现了“从p的证明得到p的证明”的要求。

2. 当p不成立时的情况 #

在构造逻辑里，“p不成立”意味着p这个类型没有任何元素（即不存在p的证明）。此时p → p依然成立，核心原因是空真（vacuous truth）：

• 当定义域（p）是空集时，从空集到自身的函数天然存在——因为根本不会有输入需要处理，这个函数的“承诺”（给输入就返回输出）永远不会被打破。
• 对应到逻辑上，就是“如果p成立则p成立”这个命题，在p本身不成立时，不会有反例，所以命题为真。

3. 澄清“证明即程序，蕴含即函数”的对应关系 #

这个对应是构造逻辑的核心规则：

• 命题 ↔ 类型：每个命题对应一个类型，命题的证明就是对应类型的元素。比如p是命题，p同时也是一个类型，它的元素就是能证明p成立的对象。
• 蕴含A → B ↔ 函数类型A → B：一个函数f : A → B就是A → B这个命题的证明——它接收一个A的证明（类型A的元素），输出一个B的证明（类型B的元素）。
• 经典逻辑的真值表是从“真假值”角度解释，构造逻辑是从“可构造性”角度解释，但两者在空真的结论上一致：当p为假时，p → p的真值为真。

举个具体例子：如果p是False（Lean内置的假命题，没有任何证明），那么False → False的证明依然是fun x => x——因为永远不会有人能提供False的证明x，这个函数永远不会被调用，自然满足蕴含关系。

内容的提问来源于stack exchange，提问作者Attila Károly