问题标签 [demorgans-law]

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

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

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

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

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

同样，您可以尝试显示

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

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

这是我想在这里证明的定律：

这是我的代码，直到我不知道该朝哪个方向前进：

显示的子目标和我所拥有的前提似乎是可证明的，但下一步是什么？

我试过用exfalso., 去apply H.之后。这给了我另一个前提x : X和一个子目标px。

不知道以后怎么办。谢谢您的帮助！

我们最近的课是关于德摩根定律的。我有点明白它的概念了

我遇到了有关此类法律的这一具体问题，我想澄清一下

还是应该像

我不想问我的教授这件事，因为我在这方面很糟糕，至少可以说他不是那种，呃，耐心类型的教授。

无论如何，这是我的理解，这¬(P → Q )意味着(¬P → ¬Q )两件不同的事情。这Q → P等于(¬P → ¬Q )。

然而，一个问题的答案说这Q → P是 的逻辑结果¬(P → Q )，我根本不明白。

为了进一步混淆问题，afaik¬(p → q) ⟺ p ∧ ¬q是正确的，所以我想我只是迷路了，在逻辑后果的定义中遗漏了一些东西？

任何帮助将非常感激。