0

Coq 使用建设性逻辑，这意味着如果您尝试填写德摩根定律，您最终会丢失 2。也就是说，您无法证明：

Theorem deMorgan_nand P Q (andPQ : ~(P /\ Q)) : P \/ Q.
Abort.

Theorem deMorgan_nall {A} (P : A -> Prop) (allPa : ~forall a, P a) : exists a, ~P a.
Abort.

这是有道理的，因为您必须计算它是 的左项还是右项or，而您通常无法做到这一点。

查看“建设性世界的经典数学”（https://arxiv.org/pdf/1008.1213.pdf）有定义

Definition orW P Q := ~(~P /\ ~Q).
Definition exW {A} (P : A -> Prop) := ~forall a, ~P a.

类似于德摩根定律。这提出了另一种表述。

Theorem deMorgan_nand P Q (andPQ : ~(P /\ Q)) : orW (~P) (~Q).
  hnf; intros nnPQ; destruct nnPQ as [ nnP nnQ ].
  apply nnP; clear nnP; hnf; intros p.
  apply nnQ; clear nnQ; hnf; intros q.
  apply (andPQ (conj p q)).  
Qed.

Theorem deMorgan_nall {A} (P : A -> Prop) (allPa : ~forall a, P a) : exW (fun a => ~P a).
Abort.

但是，它不适用于否定 forall。特别是，它在尝试转换~~P a为P a. 因此，尽管在 nand 情况下转换~~P为P，但它似乎不适用于 forall。您还可以显示其中的某些元素ahas P a。

同样，您可以尝试显示

Theorem deMorgan_nexn {A} (P : A -> Prop) (exPa : ~exists a, ~P a) : ~~forall a, P a.
Abort.

但是，一旦你有了论点a，结论就不再存在False，所以你不能使用~~P -> P。

那么，如果你不能证明deMorgan_nall，有没有类似的定理？还是~forall a, P a已经尽可能简化了？更一般地，当结论为False时，允许使用排中律 ( P \/ ~P)。当命题需要一个论点时，是否有任何对应物有效， P : A -> Prop而不是P : Prop？

4

1 回答 1

1

您正在寻找的原则被称为双重否定转变。一般而言，它在直觉主义逻辑中是无效的。尽管起初看起来相当无害，因为它的结论是一个双重否定的公式，它实际上是非常有效的。实际上，DNS 本质上是通过双重否定翻译来解释选择公理所需要的。

由 scubed 编辑：

所以，这意味着我必须添加一个公理来处理这种情况。使用公理，

Axiom deMorgan_allnn : forall {A} (P : A -> Prop) (allPa : forall a, ~~P a), ~~forall a, P a.

Theorem deMorgan_nall {A} (P : A -> Prop) (allPa : ~forall a, P a) : exW (fun a => ~P a).
  hnf; intros ex1; apply deMorgan_allnn in ex1.
  apply ex1; clear ex1; hnf; intros all2.
  apply (allPa all2).
Qed.
于 2021-09-05T14:19:02.293 回答