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

[[分类:谓词逻辑]][[分类:形式语言实例]]
{{非标准称呼}}
谓词语言('''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_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>C_0</math> 并入 <math>C</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>W</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>\lnot\phi</math> ， <math>\phi \in W</math>；
* <math>(\phi\odot\psi)</math> ， <math>\phi,\psi \in W, \odot \in C_2</math>；
* <math>\mathsf{Q} v \phi</math> ， <math>\mathsf{Q} \in Q, \phi \in W, v \in V</math>。
且：
* 最外层的括号可省略；
* 可以按照 <math>\forall \exists \lnot, \land, \lor, \rightarrow, \leftrightarrow</math> 的结合顺序省略括号。

==== BNF 定义 ====

<syntaxhighlight lang="bnf">
<formula> ::= <predicate> ( <terms> )
            | "¬" <formula>
            | "(" <formula> <op> <formula> ")"
            | <quantifier> <individual> <formula>
<op> ::= "∧" | "∨" | "→" | "↔"
<quantifier> ::= "∀" | "∃"
<terms> ::= <terms> "," <term>
<term> ::= <individual> | <function> "(" <terms> ")"
</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> 的元数相同。
且也按上述方式省略括号。