lean - TPIL 4.4：示例：¬ (∃ x, ¬ px) → (∀ x, px)

Question

精益定理证明的第 4.4 节显示以下内容：

example : (∀ x, p x) ↔ ¬ (∃ x, ¬ p x) := sorry

在这里，我将重点介绍从右到左的情况：

¬ (∃ x, ¬ p x) → (∀ x, p x)

方法一

我们知道我们将有一个类型的参数，¬ (∃ x, ¬ p x)所以让我们从它开始：

example : ¬ (∃ x, ¬ p x) → (∀ x, p x) := 

    (assume hnExnpx : ¬ (∃ x, ¬ p x),

        _)

我们知道我们必须返回一个类型的表达式，(∀ x, p x)所以让我们开始构造它：

example : ¬ (∃ x, ¬ p x) → (∀ x, p x) := 

    (assume hnExnpx : ¬ (∃ x, ¬ p x),

        (λ x, _))

此时我们需要返回一个类型的值，p x目前尚不清楚我们是否可以构建一个。也许我们需要尝试提出一个false值。

该函数hnExnpx返回false给定一个(∃ x, ¬ p x). 因此，让我们尝试构建其中一个，应用hnExnpx到它，然后使用false.elim：

example : ¬ (∃ x, ¬ p x) → (∀ x, p x) := 

    (assume hnExnpx : ¬ (∃ x, ¬ p x),

        (λ x,

            false.elim (hnExnpx (exists.intro x (λ hpx, _)))

        ))

现在我们又需要另一个false值了。

方法二

第 3 章提到有时需要经典逻辑。

一种幼稚的方法(em (∀ x, p x))将我们带到这里：

example : ¬ (∃ x, ¬ p x) → (∀ x, p x) := 

    (assume hnExnpx : ¬ (∃ x, ¬ p x),

        or.elim (em (∀ x, p x))

            (λ hAxpx, hAxpx)

            (λ hnAxpx : ¬ (∀ x, p x), (λ x, _))

    )

同样，我们需要一个p x值或一个false. 我们唯一的新东西是hnAxpx : ¬∀ (x : α), p x. 目前尚不清楚如何获得p x. hnAxpx确实返回 false 但我们需要 a(∀ x, p x)这是我们正在寻找的原始东西。:-)

也许这涉及更精细地使用经典逻辑？

欢迎任何建议！

---

更新

这是一种基于下面 simon1505475 评论的方法，该方法似乎有效：

示例： ¬ (∃ x, ¬ px) → (∀ x, px) :=

(assume hnExnpx : ¬ (∃ x, ¬ p x),

    (λ x, 

        or.elim (em (p x))

            (λ hpx : p x, hpx)

            (λ hnpx : ¬ p x, 

                false.elim (hnExnpx (exists.intro x (λ hpx : p x, hnpx hpx))))))

标签： lean