prolog - 证明的一阶逻辑语句。操纵量词

Question

好的，我有给定的关系：如果 F(x) 不正确，则没有任何情况满足 G(x) 和 H(y,x)。((∀x ¬F(x)) ⇒¬(∀y G(y) ˄ H(y,x)))

现在，我可以将其转换为： (∀y G(y) ˄ H(y,x))) ⇒ ((∀x F(x)) ????

如果不是，则左侧基本上必须暗示：如果 F(x) 不正确.... 没有提及 For All 或 Existential 量词。我可以把否定放在量词之外，即把它写成 (¬(∀x F(x))，因为这让工作更容易？？？

Answer 1

我不确定这是正确的地方，但是，不，你不能。将否定移出会改变量词。此外，初始公式可能不是您想要的：最后一个 x 是一个自由变量。