单独的 EXISTS 子句的 skolemization 是如何工作的？

Question

如果我有一个像这样的公式：

FAx FAy (Ez(!A(x,z) v !A(y,z)) v B(x,y))

(FA = For All / E = Exists)

skolemization 的规则是这样的：

1. 如果 E 在 FA 外部，则替换为常量，或者
2. 如果 E 在 FA 内部，则替换为包含来自外部的所有变量的新函数FA 作为论据。

那么在这种情况下我该怎么办呢？ 我可以删除 Exists 量词还是用常量替换它？

谢谢！

Answer 1

首先使用标准符号来写：

∀x∀y(∃z(!A(x,z)∨!A(y,z))∨B(x,y))

现在，应用第二个 skolemization 规则：

∀x∀y((!A(x,f(x,y))∨!A(y,f(x,y)))∨B(x,y))

所以我用包含来自外部的所有变量的函数替换了 ∃z 。

现在，这仍然不是 Skolem 范式，因为它不是合取 prenex 范式：公式仍然使用大量析取 (∨)。 删除这些由您决定。