如何表示∀X ∃Y r(X， Y )， ∃X ∀Y r(X， Y)?

Question

我想知道如何表达公式

• ∀X ∃Y r(X， Y);
• ∃X ∀Y r(X， Y)

在序言中。 (我的理解是Prolog应该能够表达这些公式，我在Prolog教科书中找不到类似的东西。

---

更新

我从j4n bur53的信息性回答中了解到，在Prolog中，我的问题的答案在某种程度上取决于r的性质，或者更具体地说，取决于r的论点所属集合的性质。

因此，为了具体起见，下面我将描述我目前感兴趣的两个案例(并且相当规范)。 (碰巧的是，对于这两种情况∀X ∃Y r(X， Y) 为真，∃X ∀Y r(X， Y) 为假。

案例 1让我们r以下两个事实(仅此而已)明确给出：

r(1, 2).
r(2, 1).

情况 2设r≤(正)自然数N= {1， 2， 3， ...}。 因此r(1, Y)对于所有允许的Y实例化都是正确的，但是没有X的实例化，以至于r(X, Y)对于Y的所有实例都是真的。

Answer 1

最简单的方法是使用与域相关的量词，假设 X 和 Y 来自域 a(.) 和 b(.)。然后，您可以按如下方式表示：

∀X (a(X) -> ∃Y (b(Y) & r(X, Y)))         (1) 
∃X (a(X) & ∀Y (b(Y) -> r(X, Y)))         (2)

现在的连词 (&)/2 直接是 Prologs 连词 (，)/2。对于含义(->)/2，观察以下逻辑等价A -> B == ~(A & ~B)。

因此，如果我们允许否定作为否定(~)/1的失败(+)/1，我们可以定义一个元谓词，这是在许多Prolog系统(例如SWI-Prolog)中预定义的，如下所示：

forall(F, G) :- + (F, + G).

因此，如果我们接受此处的所有转换，那么最终这两个查询将相当于以下Prolog查询。

?- forall(a(X), (b(Y),r(X,Y))).
?- a(X), forall(b(Y), r(X,Y)).

该方法通常适用于数据日志，但在以下情况下无效：

• 如果 a(.) 或 b(.) 是无限的。
• 如果 r(.，.) 有进一步的参数，即对失败的否定会丢弃绑定。
• 如果需要经典推理，即对失败的否定在这里太弱
了
• 如果涉及约束，我们可能希望 foreach/2 而不是 forall/2。
• 还有什么？