为什么在 skolemization 期间不能将所有存在的绑定器替换为唯一常量？

Question

当使用 skolemization 替换表达式中的存在量化变量时，顶层的任何存在边界都可以用新的全局唯一常量替换，但是如果存在是在全称量化下，则不能用常量替换。它必须被一个新的全局唯一谓词符号替换，该谓词符号应用于范围内的所有通用量化变量。

我不明白为什么一定要这样，因为新谓词符号的唯一性肯定会阻止它与除自身以外的任何其他对象统一。

Answer 1

当使用 skolemization 替换表达式中的存在量化变量时，顶层的任何存在边界都可以用新的全局唯一常量替换，但是如果存在在通用量化下，则不能用常量替换。

Answer 2

Skolemization 中的每一步都保留了公式的可满足性。如果所有存在约束的变量都被常量而不是函数代替，即使原始公式是可满足的，修改后的公式也可能是不可满足的。

考虑公式 ，其中

P

是具有自由变量

x

和

y

的一阶公式。如果您简单地将

y

替换为新的常量

c

，则得到的公式 在逻辑上更强，因为

y

允许依赖于

x

，但

c

不是。

换句话说，Skolemization 依赖于（二阶）逻辑等价 ，并且 是可满足的当且仅当 是。您的建议无效，因为 不等同于 .

具体的反例，假设

P

编码如下：

• 带运算

  *

  和恒等式群论公理

  1

  ,
• 该组至少有 2 个订单： 和

• y

  是

  x

  的倒数：

  x*y = 1

  .

那么 是可满足的，因为它表示“群中的每个元素都有一个逆元”。但是 是不可满足的，因为它表示“元素

c

是每个群元素的逆元素。”

Answer 3

全称量词下的存在量词必须用新的谓词符号代替常量的原因是因为常量只在全称量词范围内唯一，而不是全局唯一。这意味着在不同的范围内可能有另一个具有相同名称但引用不同对象的常量，这可能导致歧义或不一致。

另一方面，一个新的谓词符号可以是全局唯一的，因为它不是一个可以与其他术语统一的术语。相反，它是一个应用于范围内所有通用量化变量的符号，以创建一个新的原子公式，该公式是唯一的，并且与表达式中的任何其他原子公式不同。

换句话说，skolemization是一种消除存在量词的技术，但必须以保留表达式的逻辑结构和一致性的方式进行。对全称量词下的存在量词使用新的谓词符号而不是常量是确保结果表达式全局唯一且逻辑一致的一种方法。