Skolem 范式

Skolem范式
术语名称	Skolem范式
英语名称	Skolem normal form

对谓词公式，在前束范式基础上，将存在量词消除为个体常项或全称约束变元的函项，只留下全称量词的形式，称为 Skolem 范式(Skolem normal form)。 Skolem 范式是谓词公式的重要标准形式，其与原公式有相同可满足性，但未必逻辑等值。

定义

对前束范式 [math]\displaystyle{ \mathsf{Q}_1 x_1 \dots \mathsf{Q}_n x_n \phi }[/math] ：

• 对 [math]\displaystyle{ \mathsf{Q}_i }[/math] 中的每个存在量词，将其作用变元的每个约束出现替换为新的项，这一项由其前方每个全称量词所作用的变项和新的函项组成。
• 特别地，若前方没有出现全称量词，则替换为一个个体常项（在部分定义中，视为零元函项）。

这一过程称为 Skolem 化(Skolemization)。公式的前束范式 Skolem 化的结果称为其 Skolem 范式(Skolem normal form)。其中，替换时引入的项称为 Skolem 项(Skolem term)，其中的函项称为 Skolem 函项(Skolem function)，个体常项称为 Skolem 常项(Skolem constant)。

性质

每个谓词公式都存在与之等可满足的 Skolem 范式。

Skolem 化是一种语法转换规则，其语义关系可表述如下：

• Skolem 范式中引入了新的个体常项与函项符号，因此在为其提供解释时，须对原有的结构进行扩展，赋予这些新符号适当的指称。由于引入了新的符号，不能直接在原结构上比较两公式的真值。
• 从语义角度看：
  • 若原公式在某个解释下为真，则其中每个存在量词所约束的变元，依赖于其前方全称量词所约束的变元，都存在一个特定满足这一公式的取值。该依赖关系可对应为一个函数。若在扩展解释中，将 Skolem 范式中的常项与函项符号解释为恰好满足这些依赖关系的个体对象与函数，则 Skolem 范式在该扩展解释下也为真；否则，其真值不确定。
  • 反之，若 Skolem 范式在某个解释下为真，则可通过该解释中原公式存在量词对应变元的取值，构造出使原公式成立的赋值，从而原公式在该解释下也为真。

例子

首先，讨论 Skolem 范式前，假定该谓词逻辑已经被转换为前束范式的形式。若前束范式中的量词均为全称量词，其 Skolem 化过程不需要操作，前束范式就是 Skolem 范式。

• [math]\displaystyle{ \exists x (p(x) \land\lnot q(x)) }[/math] ：将存在量词的作用变元易字为个体常项 [math]\displaystyle{ x_0 }[/math] （根据不同规范，有的材料使用下加 0 表示常量，有的用通常代表常量的 [math]\displaystyle{ a,b,c }[/math]）并去除存在量词引导的量化表达式，得到 [math]\displaystyle{ p(x_0) \land\lnot q(x_0) }[/math] 。
• [math]\displaystyle{ \forall x \exists y \forall z (p(x, y) \land\lnot q(z)) }[/math] ：将存在量词的作用变元 [math]\displaystyle{ y }[/math] 易字，考虑到其处于全称量词引导的量化表达式 [math]\displaystyle{ \forall x }[/math] 的辖域中，需替换为项 [math]\displaystyle{ y(x) }[/math] （根据不同规范，有的材料使用原变项符号或其加上下标等构成的符号作为函项符号，有的用通常代表函项的 [math]\displaystyle{ f,g,h }[/math]），并去除存在量词引导的量化表达式，得到 [math]\displaystyle{ \forall x \forall z (p(x, y(x)) \land\lnot q(z)) }[/math] 。其中由于 [math]\displaystyle{ \exists y }[/math] 不在 [math]\displaystyle{ \forall z }[/math] 的辖域，不受到其影响。
• [math]\displaystyle{ \forall x \exists y \exists z (p(x, y, z)) }[/math] ：类似地，替换为 [math]\displaystyle{ \forall x (p(x, y(x), z(x))) }[/math] 。其中 [math]\displaystyle{ y,z }[/math] 都表达成 [math]\displaystyle{ x }[/math] 的函项，互相之间没有影响。

谓词逻辑/一阶逻辑
命题结构	项	个体词（个体常项、个体变项）、论域/个体域、函项、项、闭项
	谓词	谓词（谓词常项、谓词变项）
	量词	量词（辖域、出现）、全称量词 [math]\displaystyle{ \forall }[/math] 、存在量词 [math]\displaystyle{ \exists }[/math]
谓词公式	形式定义	谓词语言 [math]\displaystyle{ \mathcal{L}^* }[/math] 、谓词公式、闭式
	逻辑语义	结构、指派/赋值、基本语义定义、解释、满足、模型
	语义分类	普遍有效公式、可满足式、不可满足式
	语义关系	逻辑等值/逻辑等价 [math]\displaystyle{ = }[/math]/[math]\displaystyle{ \Leftrightarrow }[/math] 、逻辑蕴涵 [math]\displaystyle{ \Rightarrow }[/math]
	范式	前束范式、 Skolem 范式
	个体变项代入	可自由代入、易字、简单易字变形、易字变形
	命题变元代入	置换定理