前束范式：修订间差异

2026年1月3日 (六) 12:49的版本

前束范式
术语名称	前束范式
英语名称	prenex normal form
别名	PNF

谓词公式可以表示为逻辑等值的标准形式。全部量词都是常见量词，全部量化表达式都在最前，且量词均非否定、无取值范围、辖域覆盖到公式尾部，称为前束范式(prenex normal form, PNF)。前束范式是谓词公式的重要的标准形式。

定义

首标
术语名称	首标
英语名称	prefix

基式
术语名称	基式
英语名称	matrix
别名	母式

对谓词公式，若其具有形式 [math]\displaystyle{ \mathsf{Q}_1 x_1 \dots \mathsf{Q}_n x_n \phi }[/math] ，其中 [math]\displaystyle{ \phi }[/math] 不含量词，量词 [math]\displaystyle{ \mathsf{Q}_i \in \langle \forall, \exists \rangle }[/math] 且每个约束变项 [math]\displaystyle{ x_i }[/math] 均有在 [math]\displaystyle{ \phi }[/math] 中的出现，则称其为一个前束范式(prenex normal form, PNF)。其中 [math]\displaystyle{ \mathsf{Q}_1 x_1 \dots \mathsf{Q}_n x_n }[/math] 称为首标(prefix)， [math]\displaystyle{ \phi }[/math] 称为母式/基式(matrix)。

对谓词公式 [math]\displaystyle{ \psi }[/math] ，若有一前束范式与其逻辑等值，则称其为公式 [math]\displaystyle{ \psi }[/math] 的一个前束范式。

注：有的定义不要求约束变项均有在基式中出现。

性质

前束范式存在定理(prenex normal form theorem)：对每个公式 [math]\displaystyle{ \psi }[/math] ，都存在一个前束范式 [math]\displaystyle{ \phi }[/math] 与其逻辑等值。

转换算法

任意谓词公式都能通过以下步骤转换为前束范式。

将非常用量词通过常用量词表达：仅通过 [math]\displaystyle{ \exists,\forall }[/math] 表达。
消去非基本逻辑联结词（主要指蕴涵 [math]\displaystyle{ \rightarrow }[/math] 和等价 [math]\displaystyle{ \leftrightarrow }[/math] ）：将其他逻辑联结词替换为仅含 [math]\displaystyle{ \lnot,\land,\lor }[/math] 的表达方式。
深化否定词到否定表达式：使用德·摩根律将限定对象不是原子公式的否定符号移到原子公式前。包括析取、合取、存在量词、全称量词外的否定符号均被移到内部，经此步骤后，否定词仅能作用于原子公式。
检查各量词所作用的变项是否有重复，若存在，需要进行易字避免冲突。
量词前移，使每个量词的辖域均覆盖全公式。

例子

[math]\displaystyle{ \forall x \exists y \forall z (p(x, y) \land \lnot r(z)) }[/math]
[math]\displaystyle{ \forall x \exists y \forall z p(x, y, z) }[/math] （基式是一个原子，不需要逻辑联结词）
若允许零元谓词， [math]\displaystyle{ p \land q }[/math] （基式中全部谓词都是零元谓词，没出现个体变项，就不需要量化表达式）

反例：

[math]\displaystyle{ \lnot \forall x \exists y \forall z (p(x, y) \land \lnot r(z)) }[/math] ：其中第一个否定词作用的不是原子公式，应当放到原子公式前，即 [math]\displaystyle{ \exists x \forall y \exists z (\lnot p(x,y) \lor r(z)) }[/math] 。
[math]\displaystyle{ \forall x \exists y (p(x, y) \land \forall z r(z)) }[/math] ：量化表达式 [math]\displaystyle{ \forall z }[/math] 未提前。由于 [math]\displaystyle{ x,y }[/math] 出现在同一个原子公式中，而 [math]\displaystyle{ z }[/math] 出现在另一个里，此处 [math]\displaystyle{ \forall x \exists y }[/math] 之间存在固定顺序， [math]\displaystyle{ \forall z }[/math] 和这两个表达式的顺序不影响，可以随意放在前面、中间或后面。
[math]\displaystyle{ \exists x p(x) \land \forall x q(x) }[/math] ：也是未提前，但是由于同时出现了 [math]\displaystyle{ x }[/math] ，需要将一个进行易字处理，如 [math]\displaystyle{ \exists x \forall y (p(x) \land q(y)) }[/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 范式
	个体变项代入	可自由代入、易字、简单易字变形、易字变形
	命题变元代入	置换定理

@@ 第1行： / 第1行： @@
-[[分类:谓词逻辑]]
+[[分类:谓词逻辑]]{{DEFAULTSORT:qian2shu4fan4shi4}}
+{{#seo:
+|keywords=前束范式, 范式, PNF
+|description=本文介绍前束范式（PNF）的定义、性质与转换方法，包括这种范式作为谓词公式标准形式的概念，其结构特点及其在逻辑化简和计算机科学中的重要性。
+|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
+|published_time=2023-07-24
+}}
 {{InfoBox
 |name=前束范式
@@ 第5行： / 第11行： @@
 |aliases=PNF
 }}
-'''前束范式'''('''prenex normal form''', '''PNF''')指[[谓词公式]]的一种形式，将全部[[量词|量化表达式]]都放在最前面，且这些量词均非否定无取值范围、辖域都覆盖到公式尾部。
+[[谓词公式]]可以表示为[[逻辑等值]]的标准形式。
+全部量词都是常见量词，全部[[量词|量化表达式]]都在最前，且量词均非否定、无取值范围、辖域覆盖到公式尾部，称为'''前束范式'''('''prenex normal form''', '''PNF''')。
+前束范式是谓词公式的重要的标准形式。
 == 定义 ==
+{{InfoBox
+|name=首标
+|eng_name=prefix
+}}
+{{InfoBox
+|name=基式
+|eng_name=matrix
+|aliases=母式
+}}
 对谓词公式，若其具有形式 <math>\mathsf{Q}_1 x_1 \dots \mathsf{Q}_n x_n \phi</math> ，其中 <math>\phi</math> 不含量词，量词 <math>\mathsf{Q}_i \in \langle \forall, \exists \rangle</math> 且每个约束变项 <math>x_i</math> 均有在 <math>\phi</math> 中的出现，则称其为一个'''前束范式'''('''prenex normal form''', '''PNF''')。其中 <math>\mathsf{Q}_1 x_1 \dots \mathsf{Q}_n x_n</math> 称为'''首标'''('''prefix''')， <math>\phi</math> 称为'''母式'''/'''基式'''('''matrix''')。
 对谓词公式 <math>\psi</math> ，若有一前束范式与其逻辑等值，则称其为公式 <math>\psi</math> 的一个'''前束范式'''。
-注：有的定义不要求约束变项均有出现。
+注：有的定义不要求约束变项均有在基式中出现。
+== 性质 ==
+* '''前束范式存在定理'''('''prenex normal form theorem''')：对每个公式 <math>\psi</math> ，都存在一个前束范式 <math>\phi</math> 与其逻辑等值。
+== 转换算法 ==
-== 前束范式存在定理 ==
+任意谓词公式都能通过以下步骤转换为前束范式。
+# 将非常用量词通过常用量词表达：仅通过 <math>\exists,\forall</math> 表达。
+# 消去非基本逻辑联结词（主要指[[蕴涵]] <math>\rightarrow</math> 和[[等价（逻辑）|等价]] <math>\leftrightarrow</math> ）：将其他逻辑联结词替换为仅含 <math>\lnot,\land,\lor</math> 的表达方式。
+# 深化否定词到否定表达式：使用[[de Morgan 律（逻辑）|德·摩根律]]将限定对象不是原子公式的否定符号移到原子公式前。包括析取、合取、存在量词、全称量词外的否定符号均被移到内部，经此步骤后，否定词仅能作用于原子公式。
+# 检查各量词所作用的变项是否有重复，若存在，需要进行[[易字]]避免冲突。
+# 量词前移，使每个量词的辖域均覆盖全公式。
-对每个公式 <math>\psi</math> ，都存在一个前束范式 <math>\phi</math> 与其逻辑等值。
+== 例子 ==
-=== 构造证明 ===
+* <math>\forall x \exists y \forall z (p(x, y) \land \lnot r(z))</math>
+* <math>\forall x \exists y \forall z p(x, y, z)</math> （基式是一个原子，不需要逻辑联结词）
+* 若允许零元谓词， <math>p \land q</math> （基式中全部谓词都是零元谓词，没出现个体变项，就不需要量化表达式）
-* 消去联结词 <math>\rightarrow, \leftrightarrow</math> 。
+反例：
-* 深化否定词到否定表达式
+* <math>\lnot \forall x \exists y \forall z (p(x, y) \land \lnot r(z))</math> ：其中第一个否定词作用的不是原子公式，应当放到原子公式前，即 <math>\exists x \forall y \exists z (\lnot p(x,y) \lor r(z))</math> 。
-* 进行易字以免冲突
+* <math>\forall x \exists y (p(x, y) \land \forall z r(z))</math> ：量化表达式 <math>\forall z</math> 未提前。由于 <math>x,y</math> 出现在同一个原子公式中，而 <math>z</math> 出现在另一个里，此处 <math>\forall x \exists y</math> 之间存在固定顺序， <math>\forall z</math> 和这两个表达式的顺序不影响，可以随意放在前面、中间或后面。
-* 量词前移，使辖域覆盖全公式
+* <math>\exists x p(x) \land \forall x q(x)</math> ：也是未提前，但是由于同时出现了 <math>x</math> ，需要将一个进行易字处理，如 <math>\exists x \forall y (p(x) \land q(y))</math> 。
 {{谓词逻辑}}