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 技能目前非常生疏,但我可以快速说明为什么您的定理意味着双重否定消除。

在您的定理XunitPfun _ => 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 中适用于 和 的受限类PX一个特定的例子是 whenP是一个可判定的谓词和X一个有限类型。

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