查看“︁谓词公式”︁的源代码

[[分类:谓词逻辑]]{{DEFAULTSORT:ming4ti2yu3yan2}}
{{#seo:
|keywords=谓词公式, 合式公式, 逻辑公式, 谓词合式公式
|description=本文介绍谓词公式的定义、性质与分类，包括谓词公式作为谓词逻辑中合式公式的概念，其递归定义方法。
|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
|published_time=2023-07-15
}}
{{InfoBox
|name=谓词公式
|eng_name=predicate formula
|aliases=谓词合式公式,predicate well-formed formula,合式公式,well-formed formula,WFF,公式,formula
}}
'''谓词公式'''('''predicate formula''')是[[谓词语言]]中的'''合式公式'''，
由[[个体词（谓词逻辑）|个体词]]、[[函项]]、[[谓词]]、[[量词]]、[[逻辑联结词]]和括号按照特定语法规则构成的符号串。

== 定义 ==

谓词语言公式集 <math>\mathrm{Form}(\mathcal{L}^*)</math> 中的元素称为'''谓词合式公式'''('''predicate well-formed formula''')，简称'''合式公式'''('''well-formed formula'''，缩写为'''WFF''')或'''谓词公式'''('''predicate formula''')，或简称公式(formula)，是通过以下规则递归定义的符号串：
# [[原子公式]]：谓词和项构成的原子公式是谓词公式；
# 复合公式：
#* 若 <math>\varphi</math> 是谓词公式，则 <math>\lnot\varphi</math> 是谓词公式；
#* 若 <math>\varphi</math> 、 <math>\psi</math> 是谓词公式，则 <math>(\varphi \land \psi)</math> 、 <math>(\varphi \lor \psi)</math> 、 <math>(\varphi \rightarrow \psi)</math> 、 <math>(\varphi \leftrightarrow \psi)</math> 是谓词公式。
#* 若 <math>\varphi</math> 是谓词公式、 <math>x</math> 是个体变项，则 <math>\forall x \varphi</math> 、 <math>\exists x \varphi</math> 是谓词公式。
# 仅有限次应用规则 1 和 2 所得到的符号串是谓词公式。

为简化书写，通常省略最外层括号，并规定逻辑联结词的优先级从高到低为 <math>\lnot \forall \exists, \land, \lor, \rightarrow, \leftrightarrow</math> ，其中 <math>\land,\lor</math> 左结合。

注：
* 有些定义不提及命题常量。
* 有些定义中命题常量被归入命题变元。
* 有些定义包含[[真值]]常量[[真]]和[[假]]。
* 有些定义将真值常量视为零元联结词。

注意：谓词公式中由于可以含有个体变元的自由出现，通常不能确认其真值，因此谓词公式不是命题。

== 谓词公式的分类 ==
主条目：[[谓词公式分类]]


{{谓词逻辑}}