如何对普遍量词和存在量词的多个组合进行斯科勒化？

Question

(∀u∃v a(u,v)) ∧ (∀x∃y a(x,y)) 的 Skolemized形式是什么？

我不确定，因为有不同的Perenex标准形式：

• ∀u∃v ∀x∃y (a(u,v) ∧ a(x,y))
• ∀u∀x ∃v∃y (a(u,v) ∧ a(x,y))
• …

这将导致不同的Skolemized形式：

• ∀u ∀x (a(u,f(u)) ∧ a(x,g(u,x)))
• ∀u∀x (a(u,f(u,x)) ∧ a(x,g(u,x)))

在我看来，它们彼此不等同。或者我错了吗？

- Jojo

---

这对我来说似乎是可怕的离题。 :-) - Sergio Tulentsev

离题 - 是的，因为它与编程没有直接关系。 但是逻辑是我计算机科学课程的一部分，所以我认为这不是非常离题。;-) - Jojo

这个问题似乎不适合在此处讨论，因为它涉及到数理逻辑，更适合在math.stackexchange.com上进行讨论。 - templatetypedef

Answer 1

是的，对于给定的FO公式，前缀正常形式并不唯一，相应地，Skolem化也不唯一。一个更简单的例子是公式∃xAx → ∃yBy，其前缀形式为∀x∃y (Ax → By)和∃y∀x (Ax → By)，对应的Skolem化为∀x (¬ Ax ∨ Bf(x))和∀x (¬ Ax ∨ B a)，其中a是一个常量，这都展示了"作用域逃逸"。

现在，关键问题是这些公式的非等价是否对您的特定问题有影响。如果有影响，也许Skolem化不是最好的工具：Skolem化是一个旨在保持公式可满足性的过程，有时会牺牲等价性。

（在任何情况下，看看为什么单个公式的不同Skolem化是等价的是一个很好的练习，即使只是以上面的例子为例）。

- Francois G

---

我正在思考这个问题，因为我有一个更加复杂的问题需要解决。我的意图是使用推理来证明知识库是否能导出给定的假设。因此，我试图用resolution来反驳基本公式"A ∧ B ∧ ¬C"。我听说可以逐个skolemize公式的各个部分（1. "A"、2. "B"和3. "¬C"），然后把它们组合在一起。但我不知道这是否正确，如果正确的话，为什么？是什么让我能够这样做？我可以想到，如果进行部分skolemization，然后重新排列∀s/∃s并skolemize剩余部分，但我不知道是否可以这样做... - Jojo