计算机科学家逻辑/谓词逻辑/语法

定义 1（谓词逻辑的语法 - 项）

假设一个

• 可数的函数符号集 $\{f{_{i}}^{k}\mid i,k=1,2,3,\cdots \}$
• 一个可数的 $\{x_{i}\mid i=1,2,3,\cdots \}$

项的集合由以下归纳定义

• 变量 $x_{i}$ 是项。
• 如果 $t_{1},\cdots ,t_{k}$ 是项，而 $f_{i}^{k}$ 是一个函数符号，那么 $f_{i}^{k}(t_{1},\cdots ,t_{k})$ 是一个项。

类型为 $f_{i}^{0}()$ 的项是特殊的项，它们被称为常量。在这种情况下，我们省略括号并将其表示为 $f_{i}^{0}$。

项是上述对象的语法对应物。常量将表示域中的元素，而函数符号将表示引用这些对象的一种方式。

以下定义介绍了公式。

定义 2（谓词逻辑的语法 - 公式）

假设一个可数的谓词符号集 $\{p_{i}^{k}\mid i=1,2,3,\cdots \}$。公式（良构）的集合由以下归纳定义

• 如果 $t_{1},\cdots ,t_{k}$ 是项，而 $P_{i}^{k}$ 是一个谓词符号，那么 $P_{i}^{k}(t_{1},\cdots ,t_{k})$ 是一个公式。
• 如果 $F$ 和 $G$ 是公式，那么 $(F\land G)$ 和 $(F\lor G)$ 都是公式。
• 如果 $F$ 是一个公式，那么 $\lnot F$ 是一个公式。
• 如果 $x$ 是一个变量，而 $F$ 是一个公式，那么 $\forall xF$ 和 $\exists xF$ 都是公式。

类型为 $P_{i}^{k}(t_{1},\cdots ,t_{k})$ 的公式被称为原子或原子公式。

注意，子公式的概念与命题情况完全相同 (命题逻辑的语法 (Propositional Logic)).

我们引入以下缩写，它们也将与索引一起使用

$u,v,w,x,z,$			代表变量
$a,b,c,\cdots$			代表常量
$f,g,h,\cdots$			代表函数符号
$p,q,r,\cdots$			代表谓词符号

注意，在这些缩写中，函数和谓词符号的元数被省略；我们假设它将从上下文中清楚地显现出来。

示例：假设我们想要表示以下等式，它对域中的任意元素成立

$x*(y+z)=x*y+x*z$

两个运算符 $*$ 和 $+$ 在谓词逻辑公式中表示为二元函数符号 $f_{1}^{2}$ 和 $f_{2}^{2}$，三个变量是 $x_{1},x_{2}$ 和 $x_{3}$，等价关系 $=$ 是二元谓词符号 $P_{1}^{2}$。总的来说，我们有以下谓词逻辑公式

$\forall x_{1}\forall x_{2}\forall x_{3}(P_{1}^{2}(f_{2}^{2}(x_{1},f_{1}^{2}(x_{2},x_{3})),f_{1}^{2}(f_{2}^{2}(x_{1},x_{2}),f_{2}^{2}(x_{1},x_{3}))))$

在下文中，我们将使用与命题情况相同显而易见且更宽松的符号。

定义 3：变量的绑定和自由出现

在一个公式 $F$ 中，变量 $x$ 的出现被称为绑定，如果它出现在 $F$ 的一个子公式中，该子公式的形式为 $\exists x\;G$ 或 $\forall x\;G$。否则我们称这个出现为自由出现。

一个公式，如果它不包含一个变量的自由出现，就被称为闭合的。

示例： 以下公式包含 $x$ 和 $y$ 的自由出现和绑定出现。

$\forall z(Q(z)\land \forall x(P(x,y))\lor \exists y(P(x,y)))$