如何庄严化全称量词和存在量词的多种组合？答案

【问题标题】：How to skolemize multiple combinations of universal and existential quantifieres?如何庄严化全称量词和存在量词的多种组合？
【发布时间】：2012-01-28 10:22:46
【问题描述】：

(∀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)))

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

【问题讨论】：

对我来说似乎很糟糕:-)
Offtopic - 是的，因为它与编程没有直接关系。但是逻辑是我学习计算机科学课程的一部分，所以我认为这不是可怕的题外话。 ;-)
这个问题似乎跑题了，因为它是关于数学逻辑的，这在 math.stackexchange.com 上更合适。

标签： math logic theory quantifiers

【解决方案1】：

是的，prenex 范式对于给定的 FO 公式不是唯一的，并且，相应地，Skolemizations 并不是唯一的。一个更简单的例子同样的“范围逃逸”我认为你试图展示的是公式∃xAx → ∃yBy，前缀形式为 ∀x∃y (Ax → By) 和 ∃y∀x (Ax → By)，分别 skolemizations ∀x (¬ Ax ∨ Bf(x)) 和 ∀x (¬ Ax ∨ B a)，带有一个常数。

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

（无论如何，这是一个很好的练习，可以了解为什么不同的 skolemization 如果仅在上面的示例中，单个公式的

【讨论】：

我正在考虑这个问题，因为我有一个更复杂的问题，我试图解决。目的是使用分辨率来证明知识库是否可以接受给定的假设。所以我试图用分辨率来反驳的基本公式是“A ∧ B ∧ ¬C”。我听说，我可以将公式的各个部分一个一个地计算出来（1.“A”，2.“B”和 3.“¬C”），然后将它们放在一起。但我不知道这是不是真的，如果是，为什么？是什么让我能够做到这一点？我可以想到，如果我做一个部分 skolemization，然后重新排列 ∀s/∃s 并将其余部分 skolemize，但我不知道我是否可以这样做......