如何表达∀X ∃Y r(X, Y), ∃X ∀Y r(X, Y)？

Question

我想知道如何表达公式

在序言中。（我的理解是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)).

该方法通常适用于 Datalog，但不适用于以下情况：

How does one express ∀X ∃Y r(X, Y), ∃X ∀Y r(X, Y)?