具有存在目标的通用假设中的Coq箭头类型

Question

我有以下定理要证明：

Goal (exists x, ~P x) <-> ~(forall x, P x).

分手后

unfold not. split.

第一个含义非常简单，基本上我们必须在存在量词中使用从forall引入的x

。

intros. destruct H. apply H. apply (H0 x).

但另一方面，我不能这样进行，我认为应该有一个我找不到的想法。有什么建议吗？

Answer 1

嗯，这个确实是有充分理由的：我相信它在直觉逻辑中是无法证明的。

问题，正如你所发现的，要通过逆向推理取得进展，你需要

现在提供一个证人，而要通过正向推理取得进展，你需要掌握一个荒谬的假设。所以这个目标被卡住了。

问题在于，对泛量词的否定并不能给你否定属性的存在见证。

一旦你引入经典公理，有很多方法可以证明它。这是一个笨拙的中间定律排除：

Parameter T : Type.
Parameter P : T -> Prop.
Axiom EM : forall (A : Prop), A / ~ A.
Goal (exists x, ~P x) <-> ~(forall x, P x).
Proof.
  split; intro H.
  destruct H as [x H]. intro A. apply H. easy.
  destruct (EM (exists x, ~ P x)) as [?|NE].
  easy.
  elim H. intro x. destruct (EM (P x)) as [Px|NPx].
  easy.
  elim NE. exists x. easy.
Qed.