谓词公式

来自GSXAB的知识库
谓词公式
术语名称 谓词公式
英语名称 predicate formula
别名 谓词合式公式, predicate well-formed formula, 合式公式, well-formed formula, WFF, 公式, formula

谓词公式指由个体变项、个体常项、函项、谓词、量词及逻辑联结词构成的形式合理的表达式。

定义

谓词合式公式(predicate well-formed formula),简称合式公式(well-formed formula,缩写为WFF)或谓词公式(predicate formula),或简称公式(formula),是以下列形式生成的符号串:

  1. 原子公式是为谓词公式;
  2. [math]\displaystyle{ A }[/math][math]\displaystyle{ B }[/math] 是谓词公式,则 [math]\displaystyle{ \lnot A }[/math][math]\displaystyle{ A \land B }[/math][math]\displaystyle{ A \lor B }[/math][math]\displaystyle{ A \rightarrow B }[/math][math]\displaystyle{ A \leftrightarrow B }[/math] 是谓词公式。
  3. [math]\displaystyle{ A }[/math] 是谓词公式、 [math]\displaystyle{ x }[/math] 是个体变项,则 [math]\displaystyle{ \forall x A }[/math][math]\displaystyle{ \exists x A }[/math] 是谓词公式。
  4. 仅有限次应用以上各项所得到的符号串是谓词公式。

若没有括号,五个运算符按以上出现顺序的优先级进行,相同运算符从左到右。 同时,量词表达式的优先级更高,限制接下来第一个完整的谓词公式。

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


谓词逻辑/一阶逻辑
命题结构 个体词(个体常项、个体变项)、个体域、函项、项谓词(谓词常项、谓词变项)
量词(辖域、出现)全称量词 [math]\displaystyle{ \forall }[/math]存在量词 [math]\displaystyle{ \exists }[/math]
谓词公式 解释/模型赋值
分类 普遍有效公式、可满足式、不可满足式
范式 前束范式Skolem 范式