谓词逻辑：前束范式与推理演算

本节导读

上一节学会了把句子写成谓词公式，这一节学怎么用这些公式推理。大纲这一单元后三条是：范式（前束范式、Skolem 标准形）、基本推理公式及其证明方法、推理规则与推理演算（含归结推理法）。

谓词逻辑的证明推导题，常见的有两类：给出几句自然语言前提和结论，要求先形式化再写出推理过程；或者给出公式，要求化成前束范式、Skolem 标准形，再用归结法证明。学完你应该能熟练完成这两类题，并且知道四条量词规则各自的限制条件。

前束范式

如果一个公式的所有量词都在最前面，而且每个量词的辖域都延伸到公式末尾，它就是前束范式：$Q_1 x_1 Q_2 x_2 \cdots Q_k x_k M$Q1​x1​Q2​x2​⋯Qk​xk​M，其中 $Q_i$Qi​ 是 $\forall$∀ 或 $\exists$∃，M 中不含量词。任何公式都有与它等值的前束范式，但写法不唯一。

化前束范式的步骤：一，消去 $\leftrightarrow$↔，必要时消去 $\to$→；二，用量词否定等值式把否定号移到谓词前；三，用换名规则把所有约束变元改成互不相同、也不与自由变元重名的字母；四，用辖域扩张等值式把量词逐个提到最前面。第四步要特别小心：从蕴涵的前件提出的量词要换样，从后件提出的不变。

比如 $\forall x F(x, y) \to \exists y G(x, y)$∀xF(x,y)→∃yG(x,y)：前件里 x 约束、y 自由，后件里 x 自由、y 约束，先换名得 $\forall u F(u, y) \to \exists v G(x, v)$∀uF(u,y)→∃vG(x,v)；前件的 $\forall u$∀u 提出来变成 $\exists u$∃u，后件的 $\exists v$∃v 不变，结果是 $\exists u \exists v (F(u, y) \to G(x, v))$∃u∃v(F(u,y)→G(x,v))。

Skolem 标准形

归结法要求公式里只剩全称量词，办法是把存在量词「消」掉。从前束范式出发，从左到右看每个存在量词 $\exists y$∃y：如果它左边没有全称量词，就把 y 换成一个新的个体常项 a；如果它左边有全称量词 $\forall x_1, \ldots, \forall x_k$∀x1​,…,∀xk​，就把 y 换成这些变元的新函数 $f(x_1, \ldots, x_k)$f(x1​,…,xk​)，叫 Skolem 函数。例如：

$\exists x \forall y \exists z P(x, y, z) \quad \text{化为} \quad \forall y P(a, y, f(y))$∃x∀y∃zP(x,y,z)化为∀yP(a,y,f(y))

这样得到的只含全称量词的公式，就是归结法用的 Skolem 标准形。它与原公式一般不等值，但可满足性相同：原公式不可满足，当且仅当它的 Skolem 标准形不可满足。归结法证明的正是「前提与结论的否定合起来不可满足」，所以用它不影响结论。有的教材还讲一种只含存在量词的标准形（消去全称量词、保持永真性），用途不同，答题时按题目的要求写。

基本推理公式

下面这些蕴涵式都是永真的，可以直接当作推理定律使用：

推理公式	说明
$\forall x A(x) \lor \forall x B(x) \Rightarrow \forall x (A(x) \lor B(x))$∀xA(x)∨∀xB(x)⇒∀x(A(x)∨B(x))	反方向不成立
$\exists x (A(x) \land B(x)) \Rightarrow \exists x A(x) \land \exists x B(x)$∃x(A(x)∧B(x))⇒∃xA(x)∧∃xB(x)	反方向不成立
$\forall x (A(x) \to B(x)) \Rightarrow \forall x A(x) \to \forall x B(x)$∀x(A(x)→B(x))⇒∀xA(x)→∀xB(x)	全称对蕴涵只能单向分配
$\forall x (A(x) \to B(x)) \Rightarrow \exists x A(x) \to \exists x B(x)$∀x(A(x)→B(x))⇒∃xA(x)→∃xB(x)	同上
$\exists y \forall x A(x, y) \Rightarrow \forall x \exists y A(x, y)$∃y∀xA(x,y)⇒∀x∃yA(x,y)	量词交换只有这一个方向

证明一个推理公式成立，可以用下面的推理规则写出证明；证明它不成立，就构造一个使前件真、后件假的解释。

四条量词推理规则

规则	形式	使用条件
全称指定（US）	由 $\forall x A(x)$∀xA(x) 得 $A(y)$A(y) 或 $A(c)$A(c)	可以指定为任意个体变项或常项，替换后不能造成新的约束
全称推广（UG）	由 $A(y)$A(y) 得 $\forall x A(x)$∀xA(x)	y 必须代表任意个体：不能是存在指定引入的，也不能在前提里自由出现
存在指定（ES）	由 $\exists x A(x)$∃xA(x) 得 $A(c)$A(c)	c 必须是证明里之前没有出现过的新常项
存在推广（EG）	由 $A(c)$A(c) 得 $\exists x A(x)$∃xA(x)	x 不能在 $A(c)$A(c) 中已经出现

写证明的套路是：先用指定规则去掉量词，回到命题逻辑里推理，最后用推广规则加回量词。有一条经验很重要：同一个常项既要做存在指定、又要做全称指定时，先做存在指定，再做全称指定。原因是存在指定要求常项是新的，先用全称指定引入了 c，后面就不能再把 $\exists x$∃x 指定成 c 了。

谓词逻辑的归结推理法

谓词逻辑的归结比命题逻辑多一步「合一」。替换是形如 $\{t_1/x_1, \ldots, t_n/x_n\}${t1​/x1​,…,tn​/xn​} 的集合，表示把变元 $x_i$xi​ 换成项 $t_i$ti​；能使两个文字变得完全相同的替换叫合一，其中最一般的那个叫最一般合一（mgu）。合一有一条限制：变元不能换成含有它自己的项，比如 x 不能换成 $f(x)$f(x)。

归结证明的步骤：一，把前提和结论的否定都化成前束范式，再化成 Skolem 标准形；二，去掉全称量词，把母式化成合取范式，拆成子句集；三，找一对谓词相同、一正一负的文字，求出 mgu，把替换作用到两个子句上再归结；四，直到得出空子句 $\square$□。例如前提 $\forall x (P(x) \to Q(x))$∀x(P(x)→Q(x)) 和 P(a)，结论 Q(a)：子句集 $\{\neg P(x) \lor Q(x), P(a), \neg Q(a)\}${¬P(x)∨Q(x),P(a),¬Q(a)}；第一、二个子句用 $\{a/x\}${a/x} 归结得 Q(a)，再与 $\neg Q(a)$¬Q(a) 归结得 $\square$□。

易错提醒

• ❌ 从蕴涵前件里提出全称量词时保持不变。✅ 前件里的 $\forall$∀ 提出来变成 $\exists$∃，$\exists$∃ 提出来变成 $\forall$∀。因为 $A \to B$A→B 等值于 $\neg A \lor B$¬A∨B，前件带着一个否定。

• ❌ 不换名就提量词，把两个量词的约束变元并成了一个。✅ 先换名，让所有约束变元互不相同。因为 $\forall x F(x) \land \exists x G(x)$∀xF(x)∧∃xG(x) 直接提成 $\forall x \exists x$∀x∃x 是错的。

• ❌ Skolem 化时把所有存在变元都换成常项。✅ 左边有全称量词的，换成这些全称变元的函数。因为 y 的取值可能随前面的 x 变化。

• ❌ 认为 Skolem 标准形与原式等值。✅ 二者只保持可满足性。因为引入的新常项、新函数是额外的假设。

• ❌ 先全称指定成 c，再把 $\exists x$∃x 也指定成 c。✅ 先存在指定，再全称指定。因为存在指定必须引入新常项。

例题精讲

例题 1（前束范式与 Skolem 标准形）

求 $\forall x (F(x) \to \exists y G(x, y)) \land \exists y H(y)$∀x(F(x)→∃yG(x,y))∧∃yH(y) 的前束范式和 Skolem 标准形。

答题要点示范：第二个 y 换名为 z：$\forall x (F(x) \to \exists y G(x, y)) \land \exists z H(z)$∀x(F(x)→∃yG(x,y))∧∃zH(z)。$\exists y$∃y 在后件里，直接提出；再把 $\exists z$∃z 提到最前，得前束范式 $\exists z \forall x \exists y ((F(x) \to G(x, y)) \land H(z))$∃z∀x∃y((F(x)→G(x,y))∧H(z))。Skolem 化：z 左边没有全称量词，换成常项 a；y 左边有 $\forall x$∀x，换成 $f(x)$f(x)，得 $\forall x ((F(x) \to G(x, f(x))) \land H(a))$∀x((F(x)→G(x,f(x)))∧H(a))。

点评：前束范式不唯一。如果把 $\exists z$∃z 放在 $\forall x$∀x 的右边，Skolem 化时 z 就要换成 $g(x)$g(x)，也对；先提存在量词，得到的 Skolem 函数更简单。

例题 2（证明推导）

所有程序员都懂算法；有的员工是程序员；所以，有的员工懂算法。设 P(x)：x 是程序员，A(x)：x 懂算法，E(x)：x 是员工，写出推理过程。

答题要点示范：前提 $\forall x (P(x) \to A(x))$∀x(P(x)→A(x))、$\exists x (E(x) \land P(x))$∃x(E(x)∧P(x))，结论 $\exists x (E(x) \land A(x))$∃x(E(x)∧A(x))。

(1) ∃x(E(x) ∧ P(x))     前提引入
(2) E(c) ∧ P(c)         (1) 存在指定
(3) ∀x(P(x) → A(x))     前提引入
(4) P(c) → A(c)         (3) 全称指定
(5) P(c)                (2) 化简
(6) A(c)                (4)(5) 假言推理
(7) E(c)                (2) 化简
(8) E(c) ∧ A(c)         (6)(7) 合取引入
(9) ∃x(E(x) ∧ A(x))     (8) 存在推广

点评：第（2）步先做存在指定，第（4）步再把全称量词指定成同一个 c，顺序不能反。

例题 3（归结推理）

用归结法证明：$\forall x (F(x) \to G(x))$∀x(F(x)→G(x))，$\forall x (G(x) \to H(x))$∀x(G(x)→H(x))，F(a) $\Rightarrow$⇒ H(a)。

答题要点示范：子句集 $\{\neg F(x) \lor G(x), \neg G(y) \lor H(y), F(a), \neg H(a)\}${¬F(x)∨G(x),¬G(y)∨H(y),F(a),¬H(a)}（第二个子句的变元换名为 y）。F(a) 与 $\neg F(x) \lor G(x)$¬F(x)∨G(x) 用 $\{a/x\}${a/x} 归结得 G(a)；G(a) 与 $\neg G(y) \lor H(y)$¬G(y)∨H(y) 用 $\{a/y\}${a/y} 归结得 H(a)；H(a) 与 $\neg H(a)$¬H(a) 归结得 $\square$□，得证。

点评：不同子句的变元互不相干，先换成不同字母再合一，可以避免把两个 x 误当成同一个。

本节小结

• 前束范式：消联结词、移否定、换名、提量词；从前件提出的量词要换样。
• Skolem 标准形：存在变元左边无全称量词换常项，有则换成那些全称变元的函数；只保持可满足性。
• 基本推理公式要记住方向：量词交换只有 $\exists y \forall x \Rightarrow \forall x \exists y$∃y∀x⇒∀x∃y。
• 四条规则：全称指定、全称推广、存在指定、存在推广；存在指定引入新常项，所以先存在指定后全称指定。
• 谓词归结：化子句集、求 mgu、归结到空子句；变元不能换成含它自己的项。