下面的定理在 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,所以我可能只是错过了一些明显的东西。
注意我很清楚这在经典逻辑中是正确的,所以我不是在寻找一个为基础系统添加额外公理的证明。