缺失的德摩根定律

Question

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，它似乎并不适用于所有。您还可以显示a的某些元素具有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?

Answer 1

您正在寻找的原则被称为双否定移位。在一般的直觉逻辑中不有效。尽管一开始看起来相当无害，因为它的结论是一个双重否定的公式，但它实际上是相当有效的。事实上，DNS本质上是通过双重否定翻译来解释选择公理所需要的。

编辑:

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

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.