缺失的德摩根定律
缺失的德摩根定律
提问于 2021-09-05 06:05:45
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.但是，这不适用于否定所有人。特别是，它在试图将~~P a转换为P a时陷入困境。因此，尽管在nand案例中将~~P转换为P，但它似乎并不适用于forall。您还可以显示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时，是否有对应的方法呢？
回答 1
Stack Overflow用户
回答已采纳
发布于 2021-09-05 14:19:02
您要寻找的原则称为。它在一般的直觉逻辑中是不成立的。尽管一开始看起来相当无害，因为它的结论是一个双重否定的公式，它实际上是相当有效的。实际上，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.页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接：
https://stackoverflow.com/questions/69060930
复制相关文章
相似问题
腾讯云开发者
