6

下面的定理在 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，所以我可能只是错过了一些明显的东西。

注意我很清楚这在经典逻辑中是正确的，所以我不是在寻找一个为基础系统添加额外公理的证明。

4

2 回答 2

7

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

我的 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)
于 2016-02-20T11:26:35.640 回答
5

你的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一个特定的例子是 whenP是一个可判定的谓词和X一个有限类型。

于 2016-02-20T11:16:46.860 回答