12

我试图（经典地）证明

~ (forall t : U, phi) -> exists t: U, ~phi

在考克。我想要做的是相反地证明它：

1. Assume there is no such t (so ~(exists t: U, ~phi))

2. Choose arbitrary t0:U

3. If ~phi[t/t0], then contradiction with (1)

4. Therefore, phi[t/t0]

5. Conclude (forall t:U, phi)

我的问题是第 (2) 和 (5) 行。我不知道如何选择 U 的任意元素，证明一些关于它的东西，并得出结论。

有什么建议（我不致力于使用对立）？

4

1 回答 1

14

为了模仿您的非正式证明，我使用经典公理 ¬¬P → P（称为 NNPP）[1]。应用后，需要同时证明FalseA : ¬(∀ x:U, φ x) 和 B : ¬(∃ x:U, φ x)。A 和 B 是你唯一可以推断的武器False。让我们试试 A [2]。所以你需要证明∀ x:U, φ x。为了做到这一点，我们采用任意的 t₀ 并尝试证明 φ t₀ 成立 [3]。现在，由于您处于经典设置[4]，您知道 φ t₀ 成立（并且它已经完成[5]）或 ¬(φ t₀) 成立。但后者是不可能的，因为它会与 B [6] 相矛盾。

Require Import Classical. 

Section Answer.
Variable U : Type.
Variable φ : U -> Prop.

Lemma forall_exists: 
    ~ (forall x : U, φ x) -> exists x: U, ~(φ x).
intros A.
apply NNPP.               (* [1] *)
intro B.
apply A.                  (* [2] *)
intro t₀.                 (* [3] *)
elim classic with (φ t₀). (* [4] *)
trivial.                  (* [5] *)
intro H.
elim B.                   (* [6] *)
exists t₀.
assumption.
Qed.
于 2010-12-11T18:02:50.317 回答