查看“︁谓词语言”︁的源代码

[[分类:谓词逻辑]]
[[分类:形式语言实例]]{{DEFAULTSORT:ming4ti2yu3yan2}}
{{#seo:
|keywords=谓词语言, 一阶语言, 谓词逻辑的形式语言, 形式语言, 谓词逻辑
|description=本文介绍谓词语言的定义、性质与语法规则，包括谓词语言作为谓词逻辑的形式语言的概念，其字母表和公式构造规则，及其在逻辑学中的基础地位。
|modified_time={{REVISIONYEAR}}-{{REVISIONMONTH}}-{{REVISIONDAY2}}
|published_time=2024-04-05
}}
{{非标准称呼}}
谓词语言('''predicate language''')，也称'''一阶语言'''('''first-order language''')，也直接称为谓词逻辑的语言(language of predicate logic)或一阶逻辑的语言(language of first-order logic)，指研究[[:分类:谓词逻辑|谓词逻辑]]的[[形式语言]]，包括[[个体词（谓词逻辑）|个体变项]]、[[函项]]、[[谓词]]、[[逻辑联结词]]和[[量词]]，有时也被称为 <math>\mathcal{L}_1</math> 、 <math>\mathcal{L}_P</math> 或 <math>\mathcal{L}^*</math>。

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

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

=== 字母表 ===

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

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

=== 规则 ===

命题语言 <math>\mathcal{L}_1</math> 中的公式集需要先定义项集 <math>T</math> ，是通过以下规则递归定义的最小集合：
* <math>v</math> ，其中 <math>v\in V</math> ，是递归终止条件，即个体词；
* <math>f(t_1, \dots, t_n)</math> ，其中 <math>f \in F_n, n \in \mathbb{N}, t_1, \dots t_n \in T</math> 。

记 <math>\mathcal{L}_1</math> 的公式集为 <math>\mathrm{Form}(\mathcal{L}_1)</math> ，其中仅包含以下几类元素：
* <math>p(t_1, \dots, t_n)</math> ，其中 <math>p\in P_n, n \in \mathbb{N}, t_1, \dots, t_n \in T</math> ，是递归终止条件，称为 <math>\mathcal{L}_1</math>-[[原子公式]]；
* <math>\lnot\phi</math> ，其中 <math>\phi \in \mathrm{Form}(\mathcal{L}_1)</math> ；
* <math>(\phi\odot\psi)</math> ，其中 <math>\phi,\psi \in \mathrm{Form}(\mathcal{L}_1), \odot \in C_2</math> ；
* <math>\mathsf{Q} v \phi</math> ，其中 <math>\mathsf{Q} \in Q, \phi \in \mathrm{Form}(\mathcal{L}_1), v \in V</math> 。

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

=== 括号省略约定 ===

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

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

==== BNF 定义 ====

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

<syntaxhighlight lang="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₂" | ...
</syntaxhighlight>

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

== 相关术语 ==

* 主逻辑运算符：递归定义中，若一个公式不是原子公式，则形式上最后使用的逻辑运算符，即联结词或量词，称为这一公式的主逻辑运算符。即 <math>\lnot\varphi</math> 中的 <math>\lnot</math> 、 <math>\mathsf{Q}v \varphi</math> 中的 <math>\mathsf{Q} \in Q</math> 以及 <math>\varphi\odot\psi</math> 中的 <math>\odot\in C_2</math> 。也有的定义中因为认为量化表达式不是逻辑联结词，使用其他说法。
* 直接子公式(direct subformula)：递归定义中，若一个公式不是原子公式，则直接递归的公式称为这一公式的直接子公式。即 <math>\lnot\varphi</math> 中的 <math>\varphi</math> 以及 <math>\varphi\odot\psi</math> 中的 <math>\varphi</math> 和 <math>\psi</math> 。
* 子公式(subformula)：对一个公式，进行递归定义。若其是原子公式，只有其本身是其子公式；若其是非原子公式，其本身及其直接子公式的任意子公式，均是其子公式。
* 真子公式(proper subformula)：对一个公式，不是其自身的子公式。
* 非逻辑符号：表示具体论域中对象及其关系、 函数的符号。非逻辑符号和特定领域绑定，决定一个公式的具体意义。包括谓词符号、函项、个体常项。
* 逻辑符号：逻辑框架中的符号，表示公式的基本逻辑结构。逻辑符号与特定领域无关，仅受推理框架中的规则影响。包括逻辑联结词、量词、个体变项、等词、辅助符号。（个体变项不是具体对象，和量词搭配使用，因此是表示结构的；另外等词是与领域无关的固定符号，因此视为逻辑符号，但也有些文献视为非逻辑符号）

== 性质 ==

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

== 语法与语义 ==

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

== 变体 ==

* 逻辑联结词部分仅使用某个[[函数完备性（逻辑联结词）|函数完备集]]、量词仅选择其中的一个。
* 研究谓词语言时，通常仅考虑可拆分谓词和个体变项的命题，看似可拆分个体常项的部分往往视为谓词的一部分。有的变体中会引入个体常项、命题常量或真值常量等。


{{谓词逻辑}}