谓词语言

请注意，这个条目所介绍的术语没有标准称呼。仅仅是为了便于描述建立条目取了一个名字。

谓词语言(predicate language)，也称一阶语言(first-order language)，也直接称为谓词逻辑的语言(language of predicate logic)或一阶逻辑的语言(language of first-order logic)，指研究谓词逻辑的形式语言，包括个体变项、函项、谓词、逻辑联结词和量词，有时也被称为 [math]\displaystyle{ \mathcal{L}_1 }[/math] 、 [math]\displaystyle{ \mathcal{L}_P }[/math] 或 [math]\displaystyle{ \mathcal{L}^* }[/math]。

谓词语言是对谓词逻辑进行的形式语言理论的分析，对应的句子或公式就是谓词公式。

形式语言定义

定义形式语言 [math]\displaystyle{ \mathcal{L}_1 }[/math] 的字母表和规则如下：

字母表

[math]\displaystyle{ \mathcal{L}_1 }[/math] 的字母表是以下集合的并集：

• 个体变项的集合 [math]\displaystyle{ V = \{v_0, v_1, \dots \} }[/math]；
• 谓词的集合 [math]\displaystyle{ P = P_0 \cup P_1 \cup \dots }[/math]
  • 其中每个 [math]\displaystyle{ P_n, n\in \mathbb{N} }[/math] 是全体 [math]\displaystyle{ n }[/math] 元谓词的集合， [math]\displaystyle{ P_n=\{p_{n1},p_{n2},\cdots\} }[/math] 。
  • 其中 [math]\displaystyle{ P_2 }[/math] 包含等词 [math]\displaystyle{ = }[/math] 。
• 函项的集合 [math]\displaystyle{ F = F_0 \cup F_1 \cup \dots }[/math]
  • 其中每个 [math]\displaystyle{ F_n, n\in \mathbb{N} }[/math] 是全体 [math]\displaystyle{ n }[/math] 元函项的集合。
• 逻辑联结词的集合 [math]\displaystyle{ C = C_1 \cup C_2 }[/math]：
  • 一元逻辑联结词的集合 [math]\displaystyle{ C_1 = \{\lnot\} }[/math]；
  • 二元逻辑联结词的集合 [math]\displaystyle{ C_2 = \{\land, \lor, \rightarrow, \leftrightarrow\} }[/math]；
• 量词的集合 [math]\displaystyle{ Q = \{ \forall, \exists \} }[/math]：
• 辅助符号的集合，包括左右括号和逗号 [math]\displaystyle{ {\color{lightgray}\{} ({\color{lightgray},} ) {\color{lightgray},} , {\color{lightgray}\}} }[/math]。

注：不同文献对谓词语言的定义可能有所差异。

• 有些定义中，“个体词”指的是下文的“项”。
• 有些定义中包括个体常项的集合，与个体变项的集合并列。
• 有些定义中区分谓词常项和谓词变项的集合。
• 有些定义将零元谓词独立作为命题变元集合，与谓词集合并列。
• 有些定义将零元谓词分拆成命题变元和命题常量的集合，与谓词集合并列。
• 有些定义中包括真值常量真和假构成的集合 [math]\displaystyle{ \{\mathrm{T},\mathrm{F}\} }[/math] 。
• 有的定义将真或假看作零元逻辑联结词 [math]\displaystyle{ C_0 = \{\top,\bot\} }[/math] 并认为 [math]\displaystyle{ C = C_0 \cup C_1 \cup C_2 }[/math] 。
• 有些定义将真或假看作命题常量集合。
• 有些定义将零元函项独立作为个体常项集合。
• 有些定义不使用逗号。
• 有些定义中包含非常用联结词。
• 有些定义可能使用不同的符号表示。

规则

命题语言 [math]\displaystyle{ \mathcal{L}_1 }[/math] 中的公式集需要先定义项集 [math]\displaystyle{ T }[/math] ，是通过以下规则递归定义的最小集合：

• [math]\displaystyle{ v }[/math] ，其中 [math]\displaystyle{ v\in V }[/math] ，是递归终止条件，即个体词；
• [math]\displaystyle{ f(t_1, \dots, t_n) }[/math] ，其中 [math]\displaystyle{ f \in F_n, n \in \mathbb{N}, t_1, \dots t_n \in T }[/math] 。

记 [math]\displaystyle{ \mathcal{L}_1 }[/math] 的公式集为 [math]\displaystyle{ \mathrm{Form}(\mathcal{L}_1) }[/math] ，其中仅包含以下几类元素：

• [math]\displaystyle{ p(t_1, \dots, t_n) }[/math] ，其中 [math]\displaystyle{ p\in P_n, n \in \mathbb{N}, t_1, \dots, t_n \in T }[/math] ，是递归终止条件，称为 [math]\displaystyle{ \mathcal{L}_1 }[/math]-原子公式；
• [math]\displaystyle{ \lnot\phi }[/math] ，其中 [math]\displaystyle{ \phi \in \mathrm{Form}(\mathcal{L}_1) }[/math] ；
• [math]\displaystyle{ (\phi\odot\psi) }[/math] ，其中 [math]\displaystyle{ \phi,\psi \in \mathrm{Form}(\mathcal{L}_1), \odot \in C_2 }[/math] ；
• [math]\displaystyle{ \mathsf{Q} v \phi }[/math] ，其中 [math]\displaystyle{ \mathsf{Q} \in Q, \phi \in \mathrm{Form}(\mathcal{L}_1), v \in V }[/math] 。

注：最后一条有些文献中也用 [math]\displaystyle{ \mathsf{Q} v, \phi }[/math] ，所以上面的辅助符号中也有逗号。

括号省略约定

为简化书写，采用以下括号省略规则：

• 最外层的括号可省略；
• 结合性（优先级）从高到低顺序为 [math]\displaystyle{ \lnot, \mathsf{Q} v, \land, \lor, \rightarrow, \leftrightarrow }[/math] ，可按照这一顺序省略括号。（[math]\displaystyle{ \land,\lor }[/math] 之间推荐不省略）
• 多个一元运算符 [math]\displaystyle{ \lnot, \mathsf{Q}v }[/math] 连续出现时，不会出现歧义，因此可以省略之间的括号。
• 相同符号的二元联结词按照 [math]\displaystyle{ \land,\lor }[/math] 为左结合， [math]\displaystyle{ \rightarrow }[/math] 为右结合的形式省略括号。 [math]\displaystyle{ \leftrightarrow }[/math] 不规定结合性，不允许省略括号。

注：有些定义中不规定 [math]\displaystyle{ \rightarrow }[/math] 为右结合，必须使用括号明确结合性。且为了可读性， [math]\displaystyle{ \rightarrow }[/math] 的括号也往往不省略。

BNF 定义

谓词语言是一种上下文无关语言，可以通过 BNF 定义。

<formula> ::= <predicate> ( <terms> )
            | "¬" <formula>
            | "(" <formula> <op> <formula> ")"
            | <quantifier> <individual> <formula>
<op>         ::= "∧" | "∨" | "→" | "↔"
<quantifier> ::= "∀" | "∃"
<terms>      ::= <terms> "," <term>
<term>       ::= <individual> | <function> "(" <terms> ")"

<predicate>  ::= "p" | "p₀" | "p₁" | "p₂" | ...
<function>   ::= "f" | "f₀" | "v₁" | "v₂" | ...
<individual> ::= "v" | "v₀" | "v₁" | "v₂" | ...

其中 <individual>,<predicate>,<function> 三个终结符分别是个体变元、谓词、函项 [math]\displaystyle{ v \in V, p \in P, f \in F }[/math] ，并限制谓词和函项的元数和后续 <terms> 的元数相同。

相关术语

• 主逻辑运算符：递归定义中，若一个公式不是原子公式，则形式上最后使用的逻辑运算符，即联结词或量词，称为这一公式的主逻辑运算符。即 [math]\displaystyle{ \lnot\varphi }[/math] 中的 [math]\displaystyle{ \lnot }[/math] 、 [math]\displaystyle{ \mathsf{Q}v \varphi }[/math] 中的 [math]\displaystyle{ \mathsf{Q} \in Q }[/math] 以及 [math]\displaystyle{ \varphi\odot\psi }[/math] 中的 [math]\displaystyle{ \odot\in C_2 }[/math] 。也有的定义中因为认为量化表达式不是逻辑联结词，使用其他说法。
• 直接子公式(direct subformula)：递归定义中，若一个公式不是原子公式，则直接递归的公式称为这一公式的直接子公式。即 [math]\displaystyle{ \lnot\varphi }[/math] 中的 [math]\displaystyle{ \varphi }[/math] 以及 [math]\displaystyle{ \varphi\odot\psi }[/math] 中的 [math]\displaystyle{ \varphi }[/math] 和 [math]\displaystyle{ \psi }[/math] 。
• 子公式(subformula)：对一个公式，进行递归定义。若其是原子公式，只有其本身是其子公式；若其是非原子公式，其本身及其直接子公式的任意子公式，均是其子公式。
• 真子公式(proper subformula)：对一个公式，不是其自身的子公式。

性质

• 递归可枚举性：命题语言的公式集是递归可枚举的。
• 唯一可读性：每个合式公式都有唯一的语法分析树。

语法与语义

以上是谓词语言的语法，仅在符号串角度定义了符合语法约定的谓词语言符号串，没有涉及其中符号的语义。这些符号串的语义需要通过解释/模型、赋值等条目定义，最终用于逻辑蕴涵等场景。见对应条目。

变体

• 逻辑联结词部分仅使用某个函数完备集、量词仅选择其中的一个。
• 引入命题常量或真值常量。

谓词逻辑/一阶逻辑
命题结构	项	个体词（个体常项、个体变项）、论域/个体域、函项、项、闭项
	谓词	谓词（谓词常项、谓词变项）
	量词	量词（辖域、出现）、全称量词 [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 范式
	个体变项代入	可自由代入、易字、简单易字变形、易字变形
	命题变元代入	置换定理