在Coq /直觉逻辑中,这种关系是否可以证明？

Question

以下定理在Coq中可证明吗？如果没有,有没有办法证明它不可证明？

Theorem not_for_all_is_exists:
    forall (X : Set) (P : X -> Prop), ~(forall x : X, ~ P x) -> (exists x: X, P x).

我知道这种相关关系是真的:

Theorem forall_is_not_exists : (forall (X : Set) (P : X -> Prop), (forall x, ~(P x)) -> ~(exists x, P x)).
Proof.
  (* This could probably be shortened, but I'm just starting out. *)
  intros X P.
  intros forall_x_not_Px.
  unfold not.
  intros exists_x_Px.
  destruct exists_x_Px as [ witness proof_of_Pwitness].
  pose (not_Pwitness := forall_x_not_Px witness).
  unfold not in not_Pwitness.
  pose (proof_of_False := not_Pwitness proof_of_Pwitness).
  case proof_of_False.
Qed.

但我不确定如果没有双重否定消除可以帮助我.我也用不同的方法来证明有问题的定理,但无济于事.我只是在学习Coq,所以我可能只是遗漏了一些明显的东西.

NB我很清楚在经典逻辑中这是正确的,所以我不是在寻找一个能够为底层系统增加额外公理的证明.

Answer 1

这是不可证明的,因为它相当于双重否定消除(和其他经典公理).

我的Coq技能目前非常生疏,但我可以很快地说明为什么你的定理意味着双重否定消除.

在你的定理,实例X来unit并P以fun _ => X一个任意的X : Prop.现在我们有~(unit -> ~ X) -> exists (u : unit), X.但由于这种平凡性unit相当于~ ~ X -> X.

向后的含义可以通过直接应用双重否定消除来证明~ ~ (exists x, P x).

我的Agda要好得多,所以我至少可以在那里显示证据(不知道这是否有用,但它可能会稍微支持我的说法):

open import Relation.Nullary
open import Data.Product
open import Data.Unit
open import Data.Empty
open import Function

?? : Set _
?? = (A : Set)(P : A ? Set) ? ¬ (? x ? ¬ P x) ? ? P

Dneg : Set _
Dneg = (A : Set) ? ¬ ¬ A ? A

to : ?? ? Dneg
to ?? A ¬¬A = proj? (?? ? (const A) (? f ? ¬¬A (f tt)))

fro : Dneg ? ??
fro dneg A P f = dneg (? P) (f ? curry)

Answer 2

您的not_for_all_is_exists主张在Coq中无法得到证明。我建议阅读Dirk Van Dalen的“逻辑和结构”第5章的开头，以进行更深入的说明。

在直觉逻辑（和系统，例如一个Coq的），以证明exists x, P x你必须提供一种方法（或算法），将构建实际的x，使得P x保持。

假设not (forall x, not (P x))大致具有“如果我假设P所有x都不成立，那么我就会自相矛盾”的解释，但这比您想要的结论要弱，建立一个模型将揭示该假设没有足够的信息来选择的见证人P。

然而，必须指出，这个原则在Coq的适用于受限制的类P和X，特定的例子是，当P是一个可判定谓词和X有限类型。