谓词逻辑

谓词逻辑(predicate logic) 也被称为 一阶逻辑(first-order logic)，相比命题逻辑更具有表现力。在谓词逻辑中，仍然满足可靠性和完备性。

谓词逻辑作为形式语言

在谓词逻辑公式中，有两个重要的概念。首先，谓词逻辑中包含了对象，这些对象由变量符号表示，或者也可以通过函数符号来表示。在谓词逻辑中，用来表示对象的表达式均称为 项(terms)；另外一个概念与真值相关，用来表示真值的表达式被称为 公式(formulas)。

谓词逻辑词汇均由三个集合组成：谓词符号集合\(\mathcal{P}\)、函数符号集合\(\mathcal{F}\)以及常数符号集合\(\mathcal{C}\)。

注意： 常数符号可以看作零元函数，即特殊的函数；因此接下来我们抛弃常数符号集合，而使用函数符号集合作为函数和常数的集合

项

项的定义如下：

• 任何的变量都是项

• 如果\(c \in \mathcal{F}\)是一个零元函数，那么\(c\)是一个项

• 如果\(t_1,t_2,\dots,t_n\)是项，并且\(f \in \mathcal{F}\)有变元\(n > 0\)，那么\(f(t_1,t_2,\dots,t_n)\)是一个项

• 除此之外均不是项

使用BNF形式记为：

\[t ::= \ x \ | \ c \ | \ f(t,\dots,t)\]

其中\(x\)在一个变量集合\(var\)上取值，\(c\)在\(\mathcal{F}\)中零元函数符号中取值，\(f\)在非零元函数符号中取值。

公式

我们递归地在\((\mathcal{F},\mathcal{P})\)上定义公式的集合，并使用基于\(\mathcal{F}\)定义的项：

• \(\bot\)是一个公式

• 任何的命题原子（或者说零元谓词）\(p\)是一个公式

• 如果 \(P \in \mathcal{P}\)是一个变元\(n \ge 1\)的谓词符号，且如果\(t_1,t_2,\dots,t_n\)是定义在\(\mathcal{F}\)上的项，那么\(P(t_1,t_2,\dots,t_n)\)是一个公式。

• 如果\(t\)和\(s\)都是\(\mathcal{F}\)上的项，则\(t = s\)是一个公式

• 如果\(\phi\)是一个公式，那么\(\neg \phi\)也是公式。

• 如果\(\phi\)和\(\psi\)是公式，那么\((\phi \wedge \psi)\)，\((\phi \vee \psi)\)和\((\phi \rightarrow \psi)\)也是公式。

• 如果\(\phi\)是一个公式且\(x\)是一个变量，那么\((\forall x \ \phi)\)和\((\exists x \ \phi)\)也是公式。

• 除此之外均不是公式

\[\begin{split}\begin{align} \phi ::= & \bot \ | \ p \ | \ P(t_1,t_2,\dots,t_n) \ |\ t = s \ | \\ & \ (\neg \phi) \ | \ (\phi \wedge \phi) \ | \ (\phi \vee \phi) \ | \ (\phi \rightarrow \phi) \ | \ (\forall x \ \phi) \ | \ (\exists x \ \phi) \end{align} \end{split}\]

其中\(P \in \mathcal{P}\)是变元数量\(n \ge 1\)的谓词符号，\(t_i\)是\(\mathcal{F}\)上的项，\(x\)是一个变量。

习惯上，\(\neg,\forall y, \exists y \)结合最紧密，\(\wedge, \vee\)次之，\(\rightarrow\)结合性最弱且是右结合的。

自由变量和约束变量

令\(\phi\)作为谓词逻辑中的公式。如果在\(\phi\)的解析树中，存在一个叶结点\(x\)，其向上的路径中没有通向\(\forall x\)或者\(\exists x\)，则称\(x\)为 自由变量(free variables) ；否则，称\(x\)为 约束变量(bound variables) 。一个变量\(x\)是约束变量当且仅当，它位于某个\(\forall x\)或\(\exists x\)的 作用域(scope) 中。

一个量词的作用域是它的子树减去任何重新引入该量词的子树。例如\(\forall x (P(x) \rightarrow \exists x Q(x))\)的作用域是\(P(x)\)。

更加形式化地，一个项\(t\)的自由变量集合\(FV(t)\)的定义如下：

• \(FV(x) = \{x\}\).

• \(FV(c) = \emptyset\).

• \(FV(f(t_1,t_2,\dots,t_n)) = FV(t_1) \cup FV(t_2) \cup \dots \cup FV(t_n)\).

进一步，公式\(\phi\)地自由变量集合\(FV(\phi)\):

• \(FV(\bot) = FV(p) = \emptyset\).

• \(FV(P(t_1,\dots,t_n)) = FV(t_1) \cup \dots \cup FV(t_n)\).

• \(FV(t = s) = FV(t)\).

• \(FV(\phi \wedge \psi) = FV(\phi \vee \psi) = FV(\phi \rightarrow \psi) = FV(\phi) \cup FV(\psi)\).

• \(FV(\forall x . \phi) = FV(\exists x . \phi) = FV(\phi) - {x}\)

替换

变量作为占位符必须引入替换的概念。

给定一个变量\(x\)，一个项\(t\)和一个公式\(\phi\),我们定义\(\phi[t/x]\)为将每个\(\phi\)中的每个出现的自由的\(x\)替换为\(t\)后的公式。

然而，这样替换可能造成麻烦，如果一个项\(t\)中含有其他的变量\(y\)，而变量在被替换的公式中是约束变量，则会导致公式的实质发生改变。

如果对于\(t\)中的任何变量\(y\)，所有待替换的自由的\(x\)均不在\(\forall y、\exists y\)的作用域中，则称\(t\)对于\(\phi\)中的\(x\)是自由的 (free for .. in ..) 。

注意：因此，在进行替换时，应当检查是否满足上述条件

更加形式化地，”在..中对于..是自由的”可以定义为：

• \(t\)在\(\bot\)中对于\(x\)是自由的

• \(t\)在\(p\)中对于\(x\)是自由的

• \(t\)在\(P(t_1,\dots,t_n)\)中对于\(x\)是自由的

• \(t\)在\(t_1 = t_2\)中对于\(x\)是自由的

• 如果\(t\)在\(\phi\)和\(\psi\)中对于\(x\)是自由的，那么\(t\)在\(\phi \wedge \psi, \phi \vee \psi , \phi \rightarrow \psi\)中对于\(x\)是自由的

• 如果\(x \not \in FV(\forall y . \phi)\)，那么\(t\)在\(\forall y . \phi\)中对于\(x\)是自由的

• 如果\(x \not \in FV(\exists y . \phi)\)，那么\(t\)在\(\exists y . \phi\)中对于\(x\)是自由的

• 如果\(x \in FV(\forall y . \phi), y \not \in FV(t)\)，并且\(t\)在\(\phi\)中对于\(x\)是自由的，则\(t\)在\(\forall y . \phi\)对于\(x\)是自由的

• 如果\(x \in FV(\exists y . \phi), y \not \in FV(t)\)，并且\(t\)在\(\phi\)对于\(x\)是自由的，则\(t\)在\(\exists y . \phi\)对于\(x\)是自由的

谓词逻辑的证明理论

自然演绎规则

相等性规则

\[\frac{}{t=t}=_i\]

\[\frac{t_1=t_2 \ \ \ \phi[t_1/x]}{\phi[t_2/x]}=_e\]

相等性的证明规则强制了自反性，对称性和传递性。对于自反性，由\(=_i\)给出，对于对称性，证明如下：

\[\begin{split}\begin{align} &1 & \ \ \ t_1 = t_2 & \ \ \ premise \\ &2 & \ \ \ t_1 = t_1 & \ \ \ =_i \\ &3 & \ \ \ t_2 = t_1 & \ \ \ =_e 1,2 \end{align}\end{split}\]

对于传递性：

\[\begin{split}\begin{align} &1 & \ \ \ t_1 = t_2 & \ \ \ premise \\ &2 & \ \ \ t_2 = t_3 & \ \ \ premise \\ &3 & \ \ \ t_1 = t_3 & \ \ \ =_e 2,1 \end{align}\end{split}\]

全称量词规则

\[\frac{\forall x \ \phi}{\phi[t/x]} \forall x_e\]

\[\begin{split}\frac{\boxed{\begin{align} & x_0 & \\ & & \vdots \\ & & \phi[x_0/x] \end{align}}}{\forall x \ \phi} \forall x_i\end{split}\]

存在量词规则

\[\frac{\phi[t/x]}{\exists x \ \phi} \exists x_i\]

\[\begin{split}\frac{\exists x \ \phi \ \boxed{ \begin{align} & x_0 & \phi[x_0/x] \\ & & \vdots \\ & & \chi \end{align} }}{\chi} \exists x_e\end{split}\]

对于全称量词的命题，将全称量词换为存在量词也成立\(\forall x \ \phi \vdash \exists x \ \phi\).

\[\begin{split}\begin{align} & 1 & \ \ \ \forall x \ \phi \ \ \ & premise \\ & 2 & \ \ \ \phi[x/x] \ \ \ & \forall x_e 1 \\ & 3 & \ \ \ \exists x \ \phi \ \ \ & \exists x_i 2 \end{align}\end{split}\]

量词等价

下面给出量词的一些等价关系：

1 .

(a) \(\neg \forall x \ \phi \dashv \vdash \exists x \ \neg \phi\)

(b) \(\neg \exists x \ \phi \dashv \vdash \forall x \ \neg \phi\)

2 . 假设\(x\)在\(\psi\)不是自由的：

(a) \(\forall x \ \phi \wedge \psi \dashv \vdash \forall x \ (\phi \wedge \psi)\)

(b) \(\forall x \ \phi \vee \psi \dashv \vdash \forall x \ (\phi \vee \psi)\)

(c) \(\exists x \phi \wedge \psi \dashv \vdash \exists x \ (\phi \wedge \psi)\)

(d) \(\exists x \ \phi \vee \psi \dashv \vdash \exists x \ (\phi \vee \psi)\)

(e) \(\forall x \ (\psi \rightarrow \phi) \dashv \vdash \phi \rightarrow \forall x \ \phi\)

(f) \(\exists x \ (\phi \rightarrow \psi) \dashv \vdash \forall x \ \phi \rightarrow \psi\)

(g) \(\forall x \ (\phi \rightarrow \psi) \dashv \vdash \exists x \ \phi \rightarrow \psi\)

(h) \(\exists x \ (\psi \rightarrow \phi) \dashv \vdash \psi \rightarrow \exists x \ \phi\)

3 .

(a) \(\forall x \ \phi \wedge \forall x \ \psi \dashv \vdash \forall x \ (\phi \wedge \psi)\)

(b) \(\exists x \ \phi \vee \exists x \ \psi \dashv \vdash \exists x \ (\phi \vee \psi)\)

谓词逻辑的语义

模型

令\(\mathcal{F}\)为函数符号集合，\(\mathcal{P}\)为谓词符号集合，每个符号有固定数量的的参数。对\((\mathcal{F},\mathcal{P})\)的模型\(\mathcal{M}\)由如下数据组成：

• 一个非空集合\(A\)，具体值宇宙

• 对于每个零元的函数符号\(f \in \mathcal{F}\)，A的一个具体的元素\(f^{\mathcal{M}}\)

• 对于每个变元数大于零的函数符号\(f \in \mathcal{F}\)，一个具体的元素\(f^\mathcal{M} : A^n \rightarrow A\)，其中\(A^n\)是\(A\)上的n元组

• 对于每个变元数大于零的谓词符号\(P \in \mathcal{P}\)，一个子集\(P^\mathcal{M} \subseteq A^n\)

下面给出一个例子：

令\(\mathcal{F} \stackrel{\text{def}}{=} \{i\}\)以及\(\mathcal{P} \stackrel{\text{def}}{=} \{R,F\}\)。其中\(i\)是常量，\(F\)是一个一元的谓词符号，而\(R\)是一个二元的谓词符号。一个模型\(\mathcal{M}\)包含了一个具体元素的集合\(A\)(在计算机中可能表示一组计算机程序的状态)。我们令\(A \stackrel{\text{def}}{=} \{a,b,c\},i^\mathcal{M}\stackrel{\text{def}}{=} a,R^\mathcal{M}\stackrel{\text{def}}{=}\{(a,a),(a,b),(a,c),(b,c),(c,c)\},F^\mathcal{M} \stackrel{\text{def}}{=} \{b,c\}\)。

公式\(\exists y \ R(i,y)\)是真的，因为在模型中，我们有\((a,a),(a,b),(a,c)\)；公式\(\neg F(i)\)是真的，因为\(i\)被解释为了\(a\)；公式\(\forall x \forall y \forall z \ (R(x,y) \wedge R(x,z) \rightarrow y = z)\)为假，因为存在\(R(a,b),R(a,c)\)但很显然\(b \not = c\)。

对于一个具体值宇宙\(A\)，环境或 查找表(look-up table) 是一个函数\(l : var \rightarrow A\)从变量集合\(var\)到\(A\)。对于这样一个\(l\)，我们将查找表记为\(l[x \mapsto a]\)，它将\(x\)映射到\(a\)以及任何其他的变量\(y\)映射到\(l(y)\)。

为一个对\((\mathcal{F},\mathcal{P})\)给定一个模型\(\mathcal{M}\)并给出一个环境\(l\)，我们为每个逻辑公式\(\phi\)定义满足关系\(\mathcal{M} \models_l \phi\)。如果\(\mathcal{M} \models_l \phi\)满足，我们称\(\phi\)对于环境\(l\)在模型\(\mathcal{M}\)下计算为真。

• \(\bot\): \(\mathcal{M} \models_l \bot\)永不成立

• \(P(..)\): 如果\(\phi\)形式为\(P(t_1,t_2,\dots,t_n)\)，那么我们通过将其中所有变量替换为它们对应的值来解释项\(t_1,t_2,\dots,t_n\)（设解释后的具体值为\(a_1,a_2,\dots,a_n\)）；即\(\mathcal{M} \models_l P(t_1,\dots,t_n)\)成立当且仅当\((a_1,\dots,a_n) \in P^\mathcal{M}\)

• \(=\): \(\mathcal{M} \models_l t_1 = t_2\)成立当且仅当\(t1,t2\)的解释\(a_1,a_2\)在\(A\)中

• \(\forall x\): 关系\(\mathcal{M} \models_l \forall x \ \psi\)成立当且仅当对于所有的\(a \in A\)，\(\mathcal{M} \models_{l[x \mapsto a]} \psi\)成立

• \(\exists x\): 同样地，\(\mathcal{M} \models_l \exists x \ \psi\)满足当且仅当存在\(a \in A\)使得\(\mathcal{M} \models_{l[x \mapsto a]} \ \psi\)也满足

• \(\neg\): 关系\(\mathcal{M} \models_l \ \neg \psi\)满足当且仅当\(\mathcal{M} \models_l \ \psi\)不成立

• \(\vee\): 关系\(\mathcal{M} \models_l \psi_1 \vee \psi_2\)成立当且仅当\(\mathcal{M} \models_l \ \psi_1\)成立或者\(\mathcal{M} \models_l \ \psi_2\)成立

• \(\wedge\): 关系\(\mathcal{M} \models_l \psi_1 \wedge \psi_2\)成立当且仅当\(\mathcal{M} \models_l \ \psi_1\)成立且\(\mathcal{M} \models_l \ \psi_2\)成立

• \(\rightarrow\): 关系\(\mathcal{M} \models_l \psi_1 \rightarrow \psi_2\)成立当且仅当\(\mathcal{M} \models_l \psi_1\)成立使得\(\mathcal{M} \models_l \psi_2\)成立

有时将\(\mathcal{M} \not \models_l \phi\)记为\(\mathcal{M} \models_l \phi\)不成立

语义蕴含

令\(\Gamma\)是一个谓词逻辑公式的集合，\(\psi\)为一个谓词逻辑公式，则：

1 . 语义蕴含\(\Gamma \models \psi\)成立当且仅当对于所有的的模型\(\mathcal{M}\)和查找表\(l\)，当\(\forall \phi \in \Gamma ,\mathcal{M} \models_l \phi \)成立时，\(\mathcal{M} \models_l \psi\)也成立

2 . 公式\(\psi\)是可满足的，当且仅当存在某个模型\(\mathcal{M}\)和环境\(l\)使得\(\mathcal{M} \models_l \psi\)成立

3 . 公式\(\psi\)是有效的当且仅当对于所有我们可以检查\(\psi\)的模型\(\mathcal{M}\)和环境\(l\)，\(\mathcal{M} \models_l \psi\)均成立

4 . 集合\(\Gamma\)是一致的或者说可满足的当且仅当存在一个模型\(\mathcal{M}\)和一个查找表\(l\)使得\(\mathcal{M} \models_l \phi\)对于所有的\(\phi \in \Gamma\)均满足

证明语义蕴含是困难的，因为我们需要检查所有可能的模型，这是不可能通过机械化完成的；然而在某些特殊情况，蕴含关系不需要考虑到实际的模型，例如量词等价（即前面的自然演绎）

语义相等

谓词逻辑的不可判定性

谓词逻辑的有效性 给定一个逻辑公式\(\phi\)，\(\models \phi\)成立还是不成立？

答案是否定的。这并不意味着某个特定的公式是无法判断有效性的，而是不存在一个通用的算法能够针对任意谓词逻辑公式有效性判定。通过problem reduction，我们可以证明另一个不可解决的问题(the post correspondence problem)，这个结论将蕴含另一个问题的可解决性，最终得到我们的我问题也是不可解决的。

谓词逻辑的表达力

虽然牺牲了对有效性，可满足行和可证明性的可判定性，但谓词逻辑远比命题逻辑更具表达力。

即便如此，仍然有一些问题是谓词逻辑无法表达的，例如图的可达性问题：我们能否找到一个谓词逻辑公式\(\phi\)其中只有\(u\)和\(v\)两个自由变量，以及\(R\)作为仅有的二元谓词符号，使得\(\phi\)在有向图中满足满足当且仅当存在一条从\(u\)到\(v\)的路径。例如：

\[R(u,v) \vee \exists x(R(u,x) \wedge R(x,v)) \vee \exists x_1 \exists x_2 (R(u,x_1) \wedge R(x_1,x_2) \wedge R(x_2,v)) \vee \dots\]

这是一个无穷公式，因此它不是 良类型的(well-formed)。我们希望得到一个具有相同含义的良类型公式。

不幸的是，事实并非如此。在此之前，先给出一个重要的定理，该定理是谓词逻辑自然演绎完备性的结果。

紧致性定理(Compactness Theorem) 让\(\Gamma\)为谓词逻辑句子的集合。如果\(\Gamma\)任意有限子集都是可满足的，那么\(\Gamma\)也是可满足的。

提示：这里一个句子指的是不包含任何自由变量的公式

通过这个定理，我们可以得到一个有用的技巧，该技巧保证了存在无穷大小的模型的存在性。

Löwenheim-Skolem 定理 令\(\psi\)是一个谓词逻辑的句子，如果对于任意的自然数\(n \ge 1\)存在\(\psi\)的一个模型，该模型有至少\(n\)个元素，那么\(\psi\)有一个模型具有无穷元素的模型。

据此可以证明可达性在谓词逻辑中是不可表达的了。

定理 可达性在谓词逻辑中是不可表达的：不存在谓词逻辑公式\(\phi\)，其中\(u,v\)为唯二自由变量以及\(R\)为唯一的谓词符号，使得\(\phi\)在有向图中满足当且仅当图中存在一条从\(u\)到\(v\)的路径。

我们令\(c\)和\(c'\)是常数，令\(\phi_n\)公式表示存在一个从\(c\)到\(c'\)长度为\(n\)的路径。特别地，我们定义\(\phi_0\)为\(c = c'\)，\(\phi_1\)为\(R(c,c')\)；对于\(n > 1\)的情况，定义：

\[\phi_n \stackrel{\text{def}}{=} \exists x_1 \dots \exists x_{n - 1}(R(c,x_1) \wedge R(x_1,x_2) \wedge \dots \wedge R(x_{n-1},c'))\]

让\(\Delta = \{ \neg\phi_i | i \ge 0\} \cup \{ \phi[c/u][c'/v]\}\).\(\Delta\)是不可满足的，因为\(\Delta\)中全部公式的合取表示不存在长度为0、1、2…的路径，但存在一个有限路径(由\(\phi[c/u][c'/v]\)给出)。不过任何\(\Delta\)的子集都是可满足的，因为任何有限长度的路径都是可能的（可以据此给出构造的模型）。根据紧致性定理，\(\Delta\)是一致的，或者说可满足的，这与前面产生矛盾。因此不可能存在这样的公式\(\phi\)。

存在二阶逻辑

一阶谓词逻辑无法表达图的可达性，我们不希望建立一个全新的体系来解决这个问题，而是希望能够最大化地使用谓词逻辑，在此基础上进行提升。我们将量词不仅仅应用于变量，而是进一步将其应用到谓词上。

\[\exists P \phi\]

其中\(\phi\)是一个谓词逻辑公式，并包含了\(P\)，我们给出一个例子。

\[\exists P \forall x \forall y \forall z (C_1 \wedge C_2 \wedge C_3 \wedge C_4)\]

其中\(C_i\)是一个Horn子句：

\[\begin{split}& C_1 \stackrel{\text{def}}{=} P(x,x) \\ & C_2 \stackrel{\text{def}}{=} P(x,y) \wedge P(y,z) \rightarrow P(x,z) \\ & C_3 \stackrel{\text{def}}{=} P(u,v) \rightarrow \bot \\ & C_4 \stackrel{\text{def}}{=} R(x,y) \rightarrow P(x,y)\end{split}\]

如果将\(R\)和\(P\)看作集合状态上的两个转移关系，那么\(C_4\)表示任何的\(R\)边都是\(P\)边；\(C_1\)表示\(P\)是自反的；\(C_2\)表示\(P\)是传递的；\(C_3\)保证了不存在\(u\)到\(v\)的\(P\)路径。

考虑一个模型\(\mathcal{M}\)其包含了\(\phi\)中除了\(P\)的所有的函数和谓词符号的解释，让\(\mathcal{M}_\mathcal{T}\)在原始的模型上增强一个对于\(P\)的解释\(T \subseteq A \times A\)，也就是\(P^{\mathcal{M}_\mathcal{T}}\)。我们知道，对于任意的查找表\(l\)：

\[\mathcal{M} \models_l \exists P \phi \ \ \ \ iff \ \ \ \ 对于某个 \ T \subseteq A \times A, \mathcal{M}_\mathcal{T} \models_l \phi\]

上述公式成立当且仅当一个有向图中，不存在从\(u\)到\(v\)的路径。这对应着 不可达性(unreachability)。

全称二阶逻辑

我们将存在二阶逻辑取否定，并根据de Morgan公式得到：

\[\forall P \exists x \exists y \exists z (\neg C_1 \vee \neg C_2 \vee \neg C_3 \vee \neg C_4)\]

这是全称二阶逻辑，这个公式描述了可达性。

定理 让\(\mathcal{M} = (A , R^\mathcal{M})\)为任意模型，那么上述公式在查找表\(l\)和环境\(\mathcal{M}\)中成立当且仅当\(l(u)\)是\(R\)可到达\(l(v)\)的。

提示：\(P\)是\(R\)的自反传递闭包