前束范式，前束范式什么时候换名

一、前束范式书写规范

前，两点头，横，月，刂。

二、什么是前束范式

前束范式（prenexnormalform）是数理逻辑中使用谓词逻辑所描述的形式语言的一种格式。

前束范式亦称前束式，一种谓词演算公式。指其一切量词都未被否定地处于公式的最前端且其辖域都延伸至公式的末端的谓词演算公式。设Q∈{?，?}，一个公式α是前束范式，当且仅当存在一个不含量词的公式β，使得

α=(Q1x1)(Q2x2)…(Qexe)β.

三、谓词公式的前束范式是不是唯一的

不是唯一的。

前束范式亦称前束式，一种谓词演算公式。指其一切量词都未被否定地处于公式的最前端且其辖域都延伸至公式的末端的谓词演算公式。设Q∈{?，?}，一个公式α是前束范式，当且仅当存在一个不含量词的公式β，使得

α=(Q1x1)(Q2x2)…(Qexe)β.

例如，公式(?x)[F(x)→G(x)]为一个前束范式，而(?x)[F(x)∨G(x)]→(?y)R(y)不是前束范式，与一个谓词演算公式等价的前束范式公式称为谓词演算公式的前束范式，例如，公式p→(?x)α(x)的前束范式为(?x)[p→α(x)]，此处p为一个命题变元，其所有存在量词都在全称量词的前面出现的前束范式称为斯科朗范式，又称?前束范式，一个公式α是斯科朗范式，当且仅当存在一个不含量词的公式β，使得

α=(?x1)(?x3)…(?xa)(?x1)·(?x2)…(?xe)β(a≥0,e≥0).[1]

一个公式，如果量词均在全式的开头，它们的作用域延伸到整个公式的末端，则该公式叫做前束范式(PrenexNormalForm)。

前束范式可记为下述形式，其中为或，为个体变元，A是没有量词的谓词公式。