Skolem标准型

gaunthan Posted on Nov 12 2016

? Discrete Mathematics ?

> **Skolem标准型**就是将谓词逻辑公式中的全称量词和存在量词所管辖的变量映射到Skolem函数或无参Skolem变量（常量），形成的公式。

## 前束范式
Skolem标准型是在前束范式的基础上进行变量映射的。**前束范式**的定义如下：

> A是一个前束范式，如果A中的一切量词都位于该公式的最左边（不含否定词），且这些量词的辖域都延伸到公式的末端。

将谓词公式化为前束范式的过程经常会用到**改名规则**和**量词辖域扩张和收缩定律**。

## Skolem标准型
### 定义
前束范式中消去所有的量词，则称这种形式的谓词公式为**Skolem标准型**，任何一个谓词公式都可以化为与之对应的Skolem标准型。但是，Skolem标准型可以不唯一。

### 转化过程
Skolem标准型的转化过程为：

1. 依据约束变量换名规则，首先将公式变型为前束范式；
2. 依照量词消去原则消去或者略去所有量词。

由前束范式的定义可知，前束范式最左端的所有量词的辖域延伸到整个谓词公式的结尾。此时如果某个存在量词：

- 在其他全称量词的辖域范围之内，则存在某种依赖关系。例如，$ (\forall x)(( \exists y)(P(x, y)))$可以表示“每一个人$x$都有自己的$y$年龄，那么显然，年龄$y$与人$x$有关。可以用一个函数$f(x)$描述这种依赖关系，$f(x)$把每一个$x$值映射为存在的$y$值。这样的函数叫**Skolem函数**。
- 不在任何全称量词的辖域范围之内，可以将变量映射为一个常量，该常量也可以认为是没有变量的Skolem函数。如$(\exists x)P(x)$，成为$P(a)$，其中$a$为没有在谓词公式中出现过的任意常数。

经过上述转换过程的谓词公式称为Skolem标准型。具体的**量词消去原则**为：

> - 消去存在量词“$\exists$”，即，将该量词约束的变量用任意常量($a, b$等)或任意变量的函数($f(x), g(y)$等)代替。如果存在量词左边没有任何全称量词，则只将其改写成为常量；如果左边有全称量词，消去时该变量改写为全称量词的函数。
> - 略去全称量词“$\forall$”，简单地省略掉该量词。

### 一个例子
比如现在要将下面的前束范式转为Skolem标准型：
    $$(\forall x)(\exists y)(\exists u)(\forall v)( P(a, x, y) \lor Q(v, b) \lor R(u) )$$
则其转换过程为：

- 消去$(\exists y)$。因为它左边只有$(\forall x)$，所以使用$x$的函数$f(x)$代替之，得公式为：
    $$(\forall x)(\exists u)(\forall v)( P(a, x, f(x)) \lor Q(v, b) \lor R(u) )$$
- 消去$(\exists u)$，同理使用$g(x)$代替之，得公式为：
    $$(\forall x)(\forall v)( P(a, x, f(x)) \lor Q(v, b) \lor R(g(x)) )$$
- 省略所有全称量词，得公式为：
    $$P(a, x, f(x)) \lor (Q(v, b) \lor R(g(x))$$

### Skolem定理
> 任意谓词公式$G$的Skolem标准型同$G$并不等值。