Coall /直觉逻辑中的forall和existive之间是否存在这种关系？ [英] Is this relationship between forall and exists provable in Coq/intuitionistic logic?

问题描述

以下定理在Coq中可证明吗？如果不是，是否有办法证明它不可证明？

Is the following theorem provable in Coq? And if not, is there a way to prove it isn't provable?

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

我知道这种相关关系是正确的：

I know this related relationship is true:

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，所以可能只是缺少一些明显的东西。

But I'm not sure that helps me without double negative elimination. I've also played around with proving the theorem in question, with different approaches, to no avail. I'm just learning Coq, so it could be I'm just missing something obvious, however.

N.B。我很清楚这在古典逻辑中是正确的，所以我不是在寻找为基础系统添加其他公理的证明。

N.B. I'm well aware that this is true in classical logic, so I'm not looking for a proof that adds additional axioms to the underlying system.

推荐答案

这不是可证明的，因为它等效于双重否定消除（和其他经典公理）。

It's not provable, because it's equivalent to double negation elimination (and the other classical axioms).

我的Coq技能目前非常生锈，但是我可以快速说明您的定理为何意味着消除双重否定。

My Coq skills are very rusty currently, but I can quickly illustrate why your theorem implies double negation elimination.

在您的定理中，将 X 实例化为 unit 并 P 到乐趣_ => X 表示任意 X：Prop 。现在我们有〜（unit->〜X）->存在（u：单位），X 。但是由于 unit 的琐碎性，这等效于〜〜X-> X 。

In your theorem, instantiate X to unit and P to fun _ => X for an arbitrary X : Prop. Now we have ~(unit -> ~ X) -> exists (u : unit), X. But because of the triviality of unit this is equivalent to ~ ~ X -> X.

向后蕴涵可以通过在〜〜上直接应用双重否定消除来证明（存在x ，P x）。

我的Agda更好，因此我至少可以在此处显示证明（不知道这是否有帮助） ，但可能会稍微证明我的主张）：

My Agda is much better, so I can at least show the proofs there (don't know if that's helpful, but it might back up my claims a bit):

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)

这篇关于Coall /直觉逻辑中的forall和existive之间是否存在这种关系？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！