谓词语言

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

谓词语言(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_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{ C_0 }[/math] 并入 [math]\displaystyle{ C }[/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{ W }[/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{ \lnot\phi }[/math] ， [math]\displaystyle{ \phi \in W }[/math]；
[math]\displaystyle{ (\phi\odot\psi) }[/math] ， [math]\displaystyle{ \phi,\psi \in W, \odot \in C_2 }[/math]；
[math]\displaystyle{ \mathsf{Q} v \phi }[/math] ， [math]\displaystyle{ \mathsf{Q} \in Q, \phi \in W, v \in V }[/math]。

且：

最外层的括号可省略；
可以按照 [math]\displaystyle{ \forall \exists \lnot, \land, \lor, \rightarrow, \leftrightarrow }[/math] 的结合顺序省略括号。

BNF 定义

<formula> ::= p ( <terms> ) | ¬ <formula> | ( <formula> <op> <formula> ) | <quantifier> v <formula>
<op> ::= ∧ | ∨ | → | ↔
<quantifier> ::= ∀ | ∃
<terms> ::= <terms> , <term>
<term> ::= v | f ( <terms> )

其中 [math]\displaystyle{ v \in V, p \in P, f \in F }[/math] ，并附加限制其元数和后续 <terms> 的元数相同。且也按上述方式省略括号。