math - 如何 skolemize 通用量词和存在量词的多种组合？

Question

(∀u∃v a(u,v)) ∧ (∀x∃y a(x,y)) 的斯科勒化形式是什么？

我不确定，因为可能存在不同的 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)))

在我看来，它们彼此并不等同。还是我错了？

Answer 1

是的，对于给定的 FO 公式，prenex 范式不是唯一的，并且，相应地，Skolemizations 不是唯一的。一个更简单的例子同样的“范围转义”我想你想证明的是公式∃xAx→∃yBy，具有前置形式∀x∃y(Ax→By)和∃y∀x(Ax→By)，以及相应的skolemizations∀x (¬ Ax ∨ Bf(x)) 和∀x (¬ Ax ∨ B a)，具有常数。

现在，相关的问题是那些不等价的公式对您的特定问题很重要。如果是这样，也许Skolemization 不是最适合您的工具:Skolemization是一个过程旨在保持公式的可满足性，有时以牺牲为代价等价性。

(无论如何，了解为什么不同的 skolemizations 是一个很好的练习如果仅在上面的示例中，单个公式的是可满足的)