如何在Lean中基于基础规则证明(∀ x, ¬ A x) → ¬ ∃ x, A x

这个命题是构造性成立的，不需要用到经典逻辑的反证公理，仅靠否定、全称量词、存在量词的基础定义和自然演绎规则就能完成证明。

完整tactic模式证明代码 #

theorem forall_not_imp_not_exists {α : Type} (A : α → Prop) : (∀ x, ¬ A x) → ¬ ∃ x, A x :=
begin
  -- 引入第一个前提：对任意x，A x不成立
  intro h_all_not,
  -- 否定`¬ ∃ x, A x`等价于`(∃ x, A x) → false`，因此引入存在性假设
  intro h_exists,
  -- 对存在性命题做消去：拿到满足A的具体元素a，以及A a成立的证明h_a
  cases h_exists with a h_a,
  -- 将全称前提应用到a上，得到`¬ A a`（即A a → false）
  apply h_all_not a,
  -- 直接代入A a的证明h_a，得到false，完成证明
  exact h_a,
end

基础原理说明 #

1. 首先明确Lean中核心逻辑符号的定义：
   • 否定¬ P是P → false的语法糖，代表「如果P成立就能推出矛盾」
   • 因此原命题可以等价改写为：(∀ x, A x → false) → (∃ x, A x) → false
2. 证明过程完全遵循自然演绎规则：
   • 全称量词消去：如果有∀ x, P x，对任意项a都可以得到P a
   • 存在量词消去：如果有∃ x, P x，可以得到一个具体的项a和对应的P a证明
   • 蕴含消去：如果有P → Q和P的证明，就可以得到Q的证明
3. 整个过程没有用到by_contradiction等经典逻辑公理，在直觉主义逻辑中也成立。

如果用更简洁的term模式写，证明可以直接对应逻辑推导的结构：

theorem forall_not_imp_not_exists_term {α : Type} (A : α → Prop) : (∀ x, ¬ A x) → ¬ ∃ x, A x :=
λ h_all_not ⟨a, h_a⟩, h_all_not a h_a

内容的提问来源于stack exchange，提问作者Kelly Huang