logic - 自然扣除证明 - 这有效吗？

Question

我一直在练习，但我不确定有什么方法可以检查我的工作，任何人都可以指出他们在这个证明中是否有任何错误？

标签： logicfirst-order-logic

Answer 1

我不知道你的证明中的“subcomp”是什么，以及你如何得到 2。

我不会给你详细的答案，因为它看起来像家庭作业。

您要证明的定理是合取 (AND)，这意味着您必须证明双方：P 和 ¬Q。

为了证明 P，你必须使用归约到荒谬（从 ¬A，如果你可以证明 ⊥，那么你可以证明 A），或者它的另一种形式（排除中间或双重否定）。

¬Q 更容易证明，只需使用 ¬ 规则。