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

[[分类:谓词逻辑]]
{{InfoBox
|name=谓词公式
|eng_name=predicate formula
|aliases=谓词合式公式,predicate well-formed formula,合式公式,well-formed formula,WFF,公式,formula
}}
'''谓词公式'''指由个体变项、个体常项、函项、谓词、量词及逻辑联结词构成的形式合理的表达式。

== 定义 ==

'''谓词合式公式'''('''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> 是谓词公式。
# 仅有限次应用以上各项所得到的符号串是谓词公式。
若没有括号，五个运算符按以上出现顺序的优先级进行，相同运算符从左到右。
同时，量词表达式的优先级更高，限制接下来第一个完整的谓词公式。

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


{{谓词逻辑}}