logic - 单独的 EXISTS 子句的 skolemisation 是如何工作的？

Question

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

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

（FA = 全部 / E = 存在）

skolemisation 的规则说：

1. 如果 E 在 FA 之外，则替换为常数或
2. 如果 E 在 FA 内部，则用新函数替换包含 FA 外部的所有变量作为参数。

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

谢谢！

Answer 1

首先使用标准符号编写：

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

现在，应用你的第二个 skolemisation 规则：

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

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

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