查看“︁Skolem 范式”︁的源代码

[[分类:谓词逻辑]]{{DEFAULTSORT:skolem fan4shi4}}
{{#seo:
|keywords=Skolem范式, 范式
|description=本文介绍Skolem范式的定义、性质与转换方法，包括作为谓词公式标准形式的概念，其结构特点及其在逻辑化简和计算机科学中的重要性。
|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
|published_time=2023-07-24
}}
{{InfoBox
|name=Skolem范式
|eng_name=Skolem normal form
}}
对[[谓词公式]]，在[[前束范式]]基础上，将[[存在量词]]消除为[[个体词（谓词逻辑）|个体常项]]或全称约束变元的[[函项]]，只留下[[全称量词]]的形式，称为 '''Skolem 范式'''('''Skolem normal form''')。 Skolem 范式是谓词公式的重要标准形式，其与原公式有相同可满足性，但未必逻辑等值。

== 定义 ==

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


{{谓词逻辑}}