谓词公式：修订间差异

2026年1月8日 (四) 12:26的最新版本

谓词公式
术语名称	谓词公式
英语名称	predicate formula
别名	谓词合式公式, predicate well-formed formula, 合式公式, well-formed formula, WFF, 公式, formula

谓词公式(predicate formula)是谓词语言中的合式公式，由个体词、函项、谓词、量词、逻辑联结词和括号按照特定语法规则构成的符号串。

定义

谓词语言公式集 [math]\displaystyle{ \mathrm{Form}(\mathcal{L}^*) }[/math] 中的元素称为谓词合式公式(predicate well-formed formula)，简称合式公式(well-formed formula，缩写为WFF)或谓词公式(predicate formula)，或简称公式(formula)，是通过以下规则递归定义的符号串：

原子公式：谓词和项构成的原子公式是谓词公式；
复合公式：
- 若 [math]\displaystyle{ \varphi }[/math] 是谓词公式，则 [math]\displaystyle{ \lnot\varphi }[/math] 是谓词公式；
- 若 [math]\displaystyle{ \varphi }[/math] 、 [math]\displaystyle{ \psi }[/math] 是谓词公式，则 [math]\displaystyle{ (\varphi \land \psi) }[/math] 、 [math]\displaystyle{ (\varphi \lor \psi) }[/math] 、 [math]\displaystyle{ (\varphi \rightarrow \psi) }[/math] 、 [math]\displaystyle{ (\varphi \leftrightarrow \psi) }[/math] 是谓词公式。
- 若 [math]\displaystyle{ \varphi }[/math] 是谓词公式、 [math]\displaystyle{ x }[/math] 是个体变项，则 [math]\displaystyle{ \forall x \varphi }[/math] 、 [math]\displaystyle{ \exists x \varphi }[/math] 是谓词公式。
仅有限次应用规则 1 和 2 所得到的符号串是谓词公式。

为简化书写，通常省略最外层括号，并规定逻辑联结词的优先级从高到低为 [math]\displaystyle{ \lnot \forall \exists, \land, \lor, \rightarrow, \leftrightarrow }[/math] ，其中 [math]\displaystyle{ \land,\lor }[/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 范式
	个体变项代入	可自由代入、易字、简单易字变形、易字变形
	命题变元代入	置换定理

@@ 第16行： / 第16行： @@
 == 定义 ==
-谓词语言公式集 <math>\mathrm{Form}(\mathcal{L}_0)</math> 中的元素称为'''谓词合式公式'''('''predicate well-formed formula''')，简称'''合式公式'''('''well-formed formula'''，缩写为'''WFF''')或'''谓词公式'''('''predicate formula''')，或简称公式(formula)，是以下列形式生成的符号串：
+谓词语言公式集 <math>\mathrm{Form}(\mathcal{L}^*)</math> 中的元素称为'''谓词合式公式'''('''predicate well-formed formula''')，简称'''合式公式'''('''well-formed formula'''，缩写为'''WFF''')或'''谓词公式'''('''predicate formula''')，或简称公式(formula)，是通过以下规则递归定义的符号串：
-# [[原子公式]]是为谓词公式；
+# [[原子公式]]：谓词和项构成的原子公式是谓词公式；
-# 若 <math>A</math> 、 <math>B</math> 是谓词公式，则 <math>\lnot A</math> 、 <math>A \land B</math> 、 <math>A \lor B</math> 、 <math>A \rightarrow B</math> 、 <math>A \leftrightarrow B</math> 是谓词公式。
+# 复合公式：
-# 若 <math>A</math> 是谓词公式、 <math>x</math> 是个体变项，则 <math>\forall x A</math> 、 <math>\exists x A</math> 是谓词公式。
+#* 若 <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> 左结合。
+注：
+* 有些定义不提及命题常量。
+* 有些定义中命题常量被归入命题变元。
+* 有些定义包含[[真值]]常量[[真]]和[[假]]。
+* 有些定义将真值常量视为零元联结词。
 注意：谓词公式中由于可以含有个体变元的自由出现，通常不能确认其真值，因此谓词公式不是命题。
+== 谓词公式的分类 ==
+主条目：[[谓词公式分类]]
 {{谓词逻辑}}