谓词逻辑的自然演绎

Question

长期以来，我一直被一个特定的谓词逻辑问题（使用 Coq）所困扰。我已经解决了 30-40 个谓词逻辑问题，但对于这个我就是想不通。

这就是问题所在： 〜所有x，（P（x）/（Q（x）-> T（x）））->〜所有x，T（x）。

Or in box form

任何人都可以向我发送正确的方向吗？谢谢！

编辑：

这是问题的coq代码：

Variables P Q T : D -> Prop.

Theorem pred_015 : ~all x, (P(x) \/ (Q(x) -> T(x))) -> ~all x, T(x).
Proof.
imp_i H.



Qed.

Answer 1

在我看来，您正在使用一些非常旧的 Coq 版本。 在为D 添加缺失的声明并将all 替换为forall 之后，我们得到一个看起来无法证明的声明。 但是，如果我有一组括号，我会得到一个现在可以证明的目标。见以下代码：

Variable D : Set.
Variables P Q T : D -> Prop.

Theorem pred_015 : (~forall x, (P(x) \/ (Q(x) -> T(x)))) -> ~forall x, T(x).
Proof.

现在，我认为我不应该在这里公开给出解决方案，但如果您记得 ~H 被定义为 H -> False，那就很容易了。