谓词语言

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

谓词语言(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{ \forall }[/math] 、存在量词 [math]\displaystyle{ \exists }[/math]
谓词公式	形式定义	谓词语言 [math]\displaystyle{ \mathcal{L}_1 }[/math] 、谓词公式、闭式
	逻辑语义	结构、指派/赋值、基本语义定义、解释、满足、模型
	语义分类	普遍有效公式、可满足式、不可满足式
	范式	前束范式、 Skolem 范式

形式语言定义

字母表

规则

括号省略约定

BNF 定义

相关术语

性质

语法与语义

变体