(∀u∃va(u,v)) ∧ (∀x∃ya(x,y)) 的 skolemized 形式是什么？
我不确定，因为可能有不同的 perenex 范式：
- ∀u∃v ∀x∃y (a(u,v) ∧ a(x,y))
- ∀u∀x ∃v∃y (a(u,v) ∧ a(x,y))
- …</li>
会有不同的 skolemized 形式如下：
- ∀u ∀x (a(u,f(u)) ∧ a(x,g(u,x)))
- ∀u∀x (a(u,f(u,x)) ∧ a(x,g(u,x)))
在我看来，它们并不等同于彼此。还是我在这里错了？
问问题
1710 次
1 回答
2
是的，prenex 范式对于给定的 FO 公式不是唯一的，相应地，Skolemizations 也不是唯一的。我认为您试图展示的相同“范围逃逸”的一个更简单的示例是公式∃xAx→∃yBy，前缀形式为∀x∃y（Ax→By）和∃y∀x（Ax→By），以及相应的 sklemizations ∀x (¬ Ax ∨ Bf(x)) 和 ∀x (¬ Ax ∨ B a)，具有 aa 常数。
现在，相关的问题是这些公式的不等价性是否对您的特定问题很重要。如果是这样，那么 Skolemization 可能不是最适合您的工具：Skolemization是一个旨在保持公式可满足性的过程，有时会以等效性为代价。
（无论如何，如果仅在上面的示例中，了解为什么单个公式的不同 skolemization 是可以等值的，这是一个很好的练习）
于 2011-12-27T11:45:56.977 回答