3.2 一阶逻辑等值演算

本节对应原书 PDF 第 90–96 页。定义、定理、公式、例题及其原解答逐字取自原书；解释性文字为 AI 通俗化改写；标有「解读」的引用块为 AI 补充的额外直觉。

3.2.1 一阶逻辑等值式与置换规则

定义 3.10　设 A,B 是一阶逻辑中任意两个公式,若 A\leftrightarrow B 是永真式,则称 A 与 B 是等值的. 记作 A\Leftrightarrow B,称 A\Leftrightarrow B 是等值式.

由定义 3.10 可知，判断公式 A 与 B 是否等值，等价于判断公式 A\leftrightarrow B 是否为永真式。同命题逻辑中的等值式一样，人们证明出了一些重要的等值式，由这些重要的等值式可以推演出更多的等值式来，这就是一阶逻辑等值演算的内容。

下面给出一阶逻辑中的一些基本而重要的等值式.

第一组　由于命题逻辑中的重言式的代换实例都是一阶逻辑中的永真式，因而第 2 章的 24 个等值式模式给出的代换实例都是一阶逻辑的等值式。例如：

等都是双重否定律的代换实例. 又如:

等都是蕴涵等值式的代替实例.

第二组　在一阶逻辑中，证明了下面重要的等值式.

1. 消去量词等值式

设个体域为有限集 D=\{a_1,a_2,\cdots,a_n\},则有

2. 量词否定等值式

设 A(x) 是任意的含自由出现个体变项 x 的公式,则

式(3.27)的直观解释是容易的. 对于式(1),"并不是所有的 x 都有性质 A"与"存在 x 没有性质 A"是一回事. 对于式(2),"不存在有性质 A 的 x"与"所有 x 都没有性质 A"是一回事.

3. 量词辖域收缩与扩张等值式

设 A(x) 是任意的含自由出现个体变项 x 的公式,B 中不含 x 的出现,则

4. 量词分配等值式

设 A(x),B(x) 是任意的含自由出现个体变项 x 的公式,则

进行等值演算，除使用以上重要的等值式外，还要使用以下 2 条规则.

(1) 置换规则

设 \Phi(A) 是含公式 A 的公式,\Phi(B) 是用公式 B 取代 \Phi(A) 中的所有的 A 之后的公式,若 A\Leftrightarrow B,则 \Phi(A)\Leftrightarrow \Phi(B).

一阶逻辑中的置换规则与命题逻辑中的置换规则形式上完全相同,只是在这里 A,B 是一阶逻辑公式.

(2) 换名规则

设 A 为一公式,将 A 中某量词辖域中某约束变项的所有出现及相应的指导变元,改成该量词辖域中未曾出现过的某个体变项符号,公式中其余部分不变,设所得公式为 A',则 A'\Leftrightarrow A.

例如,\forall xF(x,y)\Leftrightarrow \forall tF(t,y),但不能把 x 换成 y,写成 \forall yF(y,y).

以上给出的重要等值式及 2 个变换规则在一阶逻辑等值演算中均起重要作用，因而必须记住它们并且会灵活地运用。

如果公式中含有既约束出现又自由出现的个体变项，很容易引起混淆，给演算带来不便。对此，可以用换名规则解决这个问题。

例 3.10　将下面公式化成与之等值的公式,使其没有既是约束出现的又是自由出现的个体变项.

(1) \forall xF(x,y,z)\rightarrow \exists yG(x,y,z).

(2) \forall x(F(x,y)\rightarrow \exists yG(x,y,z)).

解　(1)

原公式中,x,y 都是既约束出现又自由出现的个体变项,只有 z 仅自由出现. 而在最后得到的公式中,x,y,z,t,w 中再无既是约束出现又是自由出现个体变项了.

(2)

例 3.11　证明:

(1) \forall x(A(x)\vee B(x))\not\Leftrightarrow \forall xA(x)\vee \forall xB(x).

(2) \exists x(A(x)\wedge B(x))\not\Leftrightarrow \exists xA(x)\wedge \exists xB(x).

其中,A(x),B(x) 为含 x 自由出现的公式.

证明　(1) 只要证明 \forall x(A(x)\vee B(x))\leftrightarrow \forall xA(x)\vee \forall xB(x) 不是永真式.

取解释 I 为: 个体域为自然数集合 \mathbf{N}. A(x) 解释成 F(x): x 是奇数,B(x) 解释成 G(x): x 是偶数. 于是左端解释成 \forall x(F(x)\vee G(x)),为真命题,而右端解释成 \forall xF(x)\vee \forall xG(x),为假命题,所以该公式存在成假解释,因而它不是永真式.

对于(2)可以类似讨论.

例 3.11 说明，全称量词 \forall 对 \vee 无分配律，存在量词 \exists 对 \wedge 无分配律。但当 B(x) 换成没有 x 出现的 B 时，则有

这是式(3.28)和式(3.29)中出现的两个等值式.

例 3.12　设个体域为 D=\{a,b,c\},将下面各公式的量词消去.

(1) \forall x(F(x)\rightarrow G(x)).

(2) \forall x(F(x)\vee \exists yG(y)).

(3) \exists x\forall yF(x,y).

解　(1)

(2)

如果不用公式(3.28)将量词 \forall x 的辖域缩小,演算过程较长. 注意,此时 \exists yG(y) 为与 x 无关的公式 B.

(3)

在演算中先消去存在量词也可以,得到结果是等值的.

例 3.13　给定解释 I 如下:

(a) 个体域 D=\{2,3\}.

(b) \bar{a}=2.

(c) \bar{f}(x) 为: \bar{f}(2)=3,\bar{f}(3)=2.

(d) \bar{G}(x,y) 为: \bar{G}(2,2)=\bar{G}(2,3)=\bar{G}(3,2)=1, \bar{G}(3,3)=0. \bar{L}(x,y) 为: \bar{L}(2,2)=\bar{L}(3,3)=1, \bar{L}(2,3)=\bar{L}(3,2)=0. \bar{F}(x) 为: \bar{F}(2)=0,\bar{F}(3)=1.

在 I 下求下列各式的真值.

(1) \forall x(F(x)\wedge G(x,a)).

(2) \exists x(F(f(x))\wedge G(x,f(x))).

(3) \forall x\exists yL(x,y).

(4) \exists y\forall xL(x,y).

解　设以上公式分别为 A,B,C,D.

(1) A\Leftrightarrow(\bar{F}(2)\wedge \bar{G}(2,2))\wedge(\bar{F}(3)\wedge \bar{G}(3,2))

\Leftrightarrow(0\wedge 1)\wedge(1\wedge 1)\Leftrightarrow 0

(2) B\Leftrightarrow(\bar{F}(\bar{f}(2))\wedge \bar{G}(2,\bar{f}(2)))\vee(\bar{F}(\bar{f}(3))\wedge \bar{G}(3,\bar{f}(3)))

\Leftrightarrow(\bar{F}(3)\wedge \bar{G}(2,3))\vee(\bar{F}(2)\wedge \bar{G}(3,2))

\Leftrightarrow(1\wedge 1)\vee(0\wedge 1)\Leftrightarrow 1

(3) C\Leftrightarrow(\bar{L}(2,2)\vee \bar{L}(2,3))\wedge(\bar{L}(3,2)\vee \bar{L}(3,3))

\Leftrightarrow(1\vee 0)\wedge(0\vee 1)\Leftrightarrow 1

(4) D\Leftrightarrow \exists y(\bar{L}(2,y)\wedge \bar{L}(3,y))

\Leftrightarrow(\bar{L}(2,2)\wedge \bar{L}(3,2))\vee(\bar{L}(2,3)\wedge \bar{L}(3,3))

\Leftrightarrow(1\wedge 0)\vee(0\wedge 1)\Leftrightarrow 0

由(3),(4)的结果也说明量词的次序不能随意颠倒.

例 3.14　证明下列各等值式.

(1) \neg \exists x(M(x)\wedge F(x))\Leftrightarrow \forall x(M(x)\rightarrow \neg F(x)).

(2) \neg \forall x(F(x)\rightarrow G(x))\Leftrightarrow \exists x(F(x)\wedge \neg G(x)).

(3) \neg \forall x\forall y(F(x)\wedge G(y)\rightarrow H(x,y))\Leftrightarrow \exists x\exists y(F(x)\wedge G(y)\wedge \neg H(x,y)).

(4) \neg \exists x\exists y(F(x)\wedge G(y)\wedge L(x,y))\Leftrightarrow \forall x\forall y(F(x)\wedge G(y)\rightarrow \neg L(x,y)).

证明

(1)

由此说明例 3.4 中(3)有两种等值的符号化形式.

(2)

由此说明例 3.4 中(4)有两种等值的符号化形式.

(3)

类似可证明(4). 由(3)可知,例 3.5 中(3)的符号化形式式(3.15)与式(3.19)是等值的. (4)的符号化形式式(3.16)与式(3.20)也是等值的.

3.2.2 一阶逻辑前束范式

定义 3.11　设 A 为一个一阶逻辑公式,若 A 具有如下形式:

则称 A 为前束范式,其中 Q_i(1\leqslant i\leqslant k) 为 \forall 或 \exists,B 为不含量词的公式.

例如,\forall x\forall y(F(x)\wedge G(y)\rightarrow H(x,y))

等公式都是前束范式,而

等都不是前束范式.

定理 3.3(前束范式存在定理)　一阶逻辑中的任何公式都存在与之等值的前束范式.

本定理的证明略去.

称与公式等值的前束范式为该公式的前束范式。本定理说明，任何公式的前束范式都是存在的，但一般说来，并不唯一。

利用公式(3.27)至公式(3.30)以及 2 条变换规则（置换规则、换名规则）就可以求出公式的前束范式.

例 3.15　求下面公式的前束范式.

(1) \forall xF(x)\wedge \neg \exists xG(x).

(2) \forall xF(x)\vee \neg \exists xG(x).

解

(1)

或者

由此可知,(1)中公式的前束范式是不唯一的. 其实,

也是它的前束范式(为什么?).

(2)

由本例可以看出以下几点:

• 由于 \forall 对 \wedge 适合分配律,所以式(1)才有只带一个量词的前束范式. 而 \forall 对 \vee 不适合分配律,因而式(2)不可能有带一个量词的前束范式.
• 在使用公式(3.28)和公式(3.29)时一定注意条件,在演算中都得到了 \forall y\neg G(y) 是不含 x 的公式 B 的条件.
• 公式的前束范式是不唯一的.

例 3.16　求下列各式的前束范式,请读者填出每一步的根据.

(1) \exists xF(x)\wedge \forall xG(x).

(2) \forall xF(x)\rightarrow \exists xG(x).

(3) \exists xF(x)\rightarrow \forall xG(x).

(4) \forall xF(x)\rightarrow \exists yG(y).

解

(1)

(2)

(3)

(4)

请读者再写出以上各式的不同形式的前束范式.

例 3.17　求下列各公式的前束范式.

(1) \forall xF(x,y)\rightarrow \exists yG(x,y).

(2) (\forall x_1F(x_1,x_2)\rightarrow \exists x_2G(x_2))\rightarrow \forall x_1H(x_1,x_2,x_3).

解　解本题时一定注意，哪些个体变项是约束出现，哪些是自由出现，特别要注意哪些既是约束出现又是自由出现的个体变项。在求前束范式时，要保证它们约束和自由出现的身份与次数都不能改变，并且不能混淆.

(1)

(2)

待核：p96 例 3.17(2) 第二行右端原书印作 \forall x_1(x_1,x_2,x_3)，疑漏谓词 H，已照原样转录。

解读：求前束范式的套路是"先换名、再内移否定、然后逐个把量词提到最前面"。换名的目的是避免把同一个字母既当约束变项又当自由变项，或者把两个不同辖域里的同名变项混成一个。