将下列语句翻译成 FOL 句子
1)亚历克斯喜欢约翰
Likes(alex, john) - 我知道这是正确的
2)每个人要么是男人要么是女人
AxAy（男人（x）v女人（y））
编辑：这更好吗？？： Az(Person(z) -> man(x) v woman(y)) 或编辑：这更好吗？？： Ax(Person(x) -> man(x) v woman( X））
3）没有人既是男人又是女人
例如（（男人（x）^ ¬女人（x））v（¬男人（x）^女人（x）））
4）Alex喜欢一个喜欢女人的男人
AxEy（喜欢（男人（x），女人（y））->喜欢（亚历克斯，男人（x）））
谢谢
编辑：对于第 3 号，我在网上找到了这个“p 和 q 的排他性析取断言 p 为真或 q 为真，但不是两者兼而有之。那么，表达排他性析取的自然但冗长的方式是(p | q) & ~(p & q)。”
如果这适用，那么我假设正确答案是 Ax( (man(x) v woman(x)) ^ ¬(man(x) & woman(x)) )
但是现在我对2和3有何不同感到困惑......
嘿，我只是想知道这些是否正确
测试一阶句子是否与非正式规范一致的一种方法是使用模型。
要执行测试，您需要：
确定你的第一个句子中有多少关系并列出它们。该列表将扮演模型的逻辑签名的角色。
现在采取一组足够大的个体，将所有有趣的属性组合分配给至少一个个体。
根据您对第一句中关系含义的理解，将属性分配给个人。
最后，对于每个普遍量化的变量，尝试将个体分配给变量并检查属性是否成立。
考虑帖子中的一个例子。
非正式说明：亚历克斯喜欢一个喜欢女人的男人
我们有
现在考虑一个结构，其中我们有一个 Alex 的个体，一个不是 Alex 的男人的个体，以及一个不是 Alex 的女人的个体。
让我们从三个开始：p1、p2、p3。
非正式规范说，亚历克斯喜欢一个男人，喜欢另一个女人。我们的模型满足这个规范。
现在考虑取自 OP 的以下语句：
AxEy(Likes( man(x), woman(y) ) -> Likes(alex, man(x) ))
该声明来自不同的语言。这里man(x)和woman(y)是一元函数而不是一元关系，所以我们不能检查这句话。
我不会进一步推测女人（y）或男人（x）是一个函数（双关语）的主题。相反，我会考虑一个不同的句子。
AxEy(Man(x) & Woman(y) & Likes( x, y ) -> Likes(alex, x ))
让我们看看如果 x=p2 和 y=p1 会发生什么。在我们的模型中，前提
Man(p2) & Woman(p3) & Likes( p2, p3 )
成立，结论
Likes(p1,p2)
也成立，因此该公式在此变量赋值下成立。
现在考虑一个不同的模型。这次有四个人：p1，p2，p3，p4。
这个模型也满足我们的非正式规范，因为 Alex 喜欢 p2 是男人，喜欢 p3 是女人。
考虑赋值 x=p4 和 y=p3。
我们的模型中的前提再次成立
Man(p4) & Woman(p3) & Likes( p4, p3 )
然而结论
Likes(p1,p4)
在我们的模型中不成立。由于x是普遍量化的，这可能是一个问题，因为该公式在此分配下不成立，但y在存在量词下。让我们看看我们是否可以找到一个赋值y，将我们的公式变成一个真实的陈述x=p4。
这确实是可能的。让y=p2.
Man(p4) & Woman(p2) & Likes( p4, p2 )
不成立，因此公式
Man(p4) & Woman(p2) & Likes( p4, p2 ) -> Likes(p1,p4)
是真的。这听起来更好，以满足我们接受的分配与非正式规范的预期含义相去甚远的公式。最初的规范显然不是在谈论一个喜欢另一个男人的男人。所以我们还没有完成。
考虑一个只有两个人的模型：p1 和 p2。
非正式规范在这个模型中不成立，所以我们的句子也应该是错误的。有四种可能的变量赋值
由于Like(x,y)在我们的模型中总是错误的，因此根据蕴含规则，前提不成立，因此公式为真。所以我们的句子在它不应该成立的模型中也是正确的。再一次，我们的一阶形式化不符合非正式规范。
这似乎是我们用来测试翻译的一个非常复杂的过程。它假定有一定的寻找反例的技能，并始终牢记非正式规范的预期含义。
让我们回顾一下我们的非正式规范
非正式说明：亚历克斯喜欢一个喜欢女人的男人
并以更容易翻译的方式重新表述
有一个Alex喜欢的男人，这个男人喜欢某个女人
这句话有两个部分与一个和连接
所以我们有
前（男人（x）和喜欢（亚历克斯，x）和艾伊（女人（y）和喜欢（x，y）））。
您喜欢所有量词都收集在一个量词前缀中的 prenex 范式。我们可以应用逻辑等价得到
ExEy（男人（x）和喜欢（亚历克斯，x）和女人（y）和喜欢（x，y））。
现在让我们检查该语句是否与上一节中每个结构中的规范一致。
由于变量是存在量化的并且规范成立，我们只需要为公式找到一个令人满意的分配。
考虑
该连词在此分配下成立。
可以使用与上一小节相同的分配。事实上，结构 1 是结构 2 的子结构。对于存在量化的陈述，我们知道，如果它在子结构中为真，那么在整个结构中也为真。
因为在我们的结构中不存在(x,y)这样的元素对，合取Likes(x,y)
Man(x) & Likes(Alex,x) & Woman(y) & Likes(x,y)
不可能是真的，所以这个陈述是假的。我们也知道结构 3 不满足我们的非正式规范，因此我们的公式通过了我们的测试。
我们的测试程序绝不是完整的。然而，它给了我们一些保证，即翻译确实是正确的。