第五章 谓词逻辑的等值和推理演算¶
否定型等值式¶
- 若给定了两个谓词公式 \(A, B\)，说 \(A\) 和 \(B\) 是等值的，如果在公式 \(A, B\) 的任一解释下，\(A\) 和 \(B\) 都有相同的真值。
- 在谓词逻辑中， 需要给出解释的内容包括:
- 论域
- 谓词变项
- 命题变项
- 函数
- 自由个体
- 在谓词逻辑中， 需要给出解释的内容包括:
- 等价的说法:
- \(A, B\) 等值当且仅当 \(A \leftrightarrow B\) 是普遍有效的公式
- 记作 \(A = B\) 或 \(A \iff B\)
由命题公式移植来的等值式¶
\[
\begin{aligned} & \neg \neg P(x)= P(x)\\ & \neg \neg(\forall x) P(x)=(\forall x) P(x)\\ & P(x) \rightarrow Q(x)=\neg P(x) \vee Q(x)\\ & (\forall x) P(x) \rightarrow(\exists x) Q(x)=\neg(\forall x) P(x) \vee(\exists x) Q(x)\\ & (P(x) \wedge Q(x)) \vee R(x)=(P(x) \vee R(x)) \wedge(Q(x) \vee R(x))\\ & ((\forall x) P(x) \wedge Q(y)) \vee(\exists z) R(z) =((\forall x) P(x) \vee(\exists z) R(z)) \wedge(Q(y) \vee(\exists z) R(z)) \end{aligned}
\]
否定型等值式（摩根律的推广）¶
\[
\begin{aligned} \neg(\forall x) P(x)=(\exists x) \neg P(x) \\ \neg(\exists x) P(x)=(\forall x) \neg P(x) \end{aligned}
\]
- 形式上看这对公式，是说否定词“\(\neg\)”可越过量词深入到量词的辖域内，但要把所越过的量词 \(\forall\) 转换为 \(\exists\)，\(\exists\) 转换为 \(\forall\)
量词分配等值式¶
量词对合取、析取的分配律¶
\[
\begin{aligned} (\forall x)(P(x) \vee q)=(\forall x) P(x) \vee q \\ (\exists x)(P(x) \vee q)=(\exists x) P(x) \vee q \\ (\forall x)(P(x) \wedge q)=(\forall x) P(x) \wedge q \\ (\exists x)(P(x) \wedge q)=(\exists x) P(x) \wedge q \end{aligned}
\]
量词对蕴涵的分配律¶
\[
\begin{aligned} (\forall x)(P(x) \rightarrow q)=(\exists x) P(x) \rightarrow q \\ (\exists x)(P(x) \rightarrow q)=(\forall x) P(x) \rightarrow q \\ (\forall x)(p \rightarrow Q(x))=p \rightarrow(\forall x) Q(x) \\ (\exists x)(p \rightarrow Q(x))=p \rightarrow(\exists x) Q(x) \end{aligned}
\]
全称量词对合取、存在量词对析取的分配律¶
\[
\begin{aligned} (\forall x)(P(x) \wedge Q(x))=(\forall x) P(x) \wedge(\forall x) Q(x) \\ (\exists x)(P(x) \vee Q(x))=(\exists x) P(x) \vee(\exists x) Q(x) \end{aligned}
\]
变元易名后的分配律¶
\[
\begin{aligned} (\forall x)(\forall y)(P(x) \vee Q(y))=(\forall x) P(x) \vee(\forall y) Q(y) \\ (\exists x)(\exists y)(P(x) \wedge Q(y))=(\exists x) P(x) \wedge(\exists y) Q(y) \end{aligned}
\]
范式¶
- 在命题逻辑里．每一公式都有与之等值的范式。
- 范式是一种统一的表达形式、当研究一个公式的特点(如永真、永假)时，范式起着重要的作用。
- 对谓词逻辑的公式来说也有范式
- 其中前束范式与原公式是等值的
- 其他范式与原公式只有较弱的关系
前束范式¶
- 前束范式：如果 \(A\) 中的一切量词都位于该公式的最左边（不含否定词）且这些量词的辖域都延伸到公式的末端，便称 \(A\) 为前束范式。
-
前束范式 \(A\) 的一般形式为
\[ \left(Q_{1} x_{1}\right) \cdots\left(Q_{n} x_{n}\right) M\left(x_{1},\cdots,x_{n}\right) \]其中 \(Q_{i}\) 为量词 \(\forall\) 或 \(\exists(i=1,\cdots,n)\)，\(M\) 称作公式 \(A\) 的 母式（基式），\(M\) 中不再有量词
-
谓词逻辑的任一公式都可化为与之等值的前束范式，但其前束范式并不唯一
- 步骤：
- 消除联结词 \(\leftrightarrow, \rightarrow\)
- 反复使用摩根律将 \(\neg\) 内移
- 使用分配等值式将量词左移
- 使用变元易名分配等值式进行变元易名
Skolem 标准形¶
- 定义：仅保留全称量词的前束形。
- 谓词逻辑的任一公式 \(A\) 都可以化作 Skolem 标准型，并且 \(A\) 是不可满足的，当且仅当其 Skolem 标准型是不可满足的。
- 这定理是说对不可满足的公式，它与其 Skolem 标准形是等值的，而一般的公式与其 Skolem 标准形并不是等值的。自然仅当 \(A\) 是不可满足的方使用 Skolem 标准形
- 求 Skolem 标准形的步骤：
- 首先要求出前束形
- 从左到右消去存在量词，设要消去 \((\exists x)\)，则将谓词 \(P\) 中出现的所有变元 \(x\) 均以论域中的某个常项 \(a\) 代入。若 \((\exists x)\) 的左边有若干全称量词 \((\forall y)\cdots(\forall z)\)，需将谓词 \(P\) 中出现的所有变元 \(x\) 均以全称量词 \(y,\cdots,z\) 的某个多元函数 \(f(y,\cdots,z)\) 代入。
- 这样便得消去全部存在量词的 Skolem 标准形
基本推理公式¶
\[
\begin{aligned} &(\forall x) P(x) \vee(\forall x) Q(x) \Rightarrow(\forall x)(P(x) \vee Q(x))\\ &(\exists x)(P(x) \wedge Q(x)) \Rightarrow(\exists x) P(x) \wedge(\exists x) Q(x)\\ &(\forall x)(P(x) \rightarrow Q(x)) \Rightarrow(\forall x) P(x) \rightarrow(\forall x) Q(x)\\ &(\forall x)(P(x) \rightarrow Q(x)) \Rightarrow(\exists x) P(x) \rightarrow(\exists x) Q(x)\\ &(\forall x)(P(x) \leftrightarrow Q(x)) \Rightarrow(\forall x) P(x) \leftrightarrow(\forall x) Q(x)\\ &(\forall x)(P(x) \leftrightarrow Q(x)) \Rightarrow(\exists x) P(x) \leftrightarrow(\exists x) Q(x)\\ &(\forall x)(P(x) \rightarrow Q(x)) \wedge(\forall x)(Q(x) \rightarrow R(x)) \Rightarrow(\forall x)(P(x) \rightarrow R(x))\\ &(\forall x)(P(x) \rightarrow Q(x)) \wedge P(a) \Rightarrow Q(a)\\ &(\forall x)(\forall y) P(x, y) \Rightarrow(\exists x)(\forall y) P(x, y)\\ &(\exists x)(\forall y) P(x, y) \Rightarrow(\forall y)(\exists x) P(x, y)\\ \end{aligned}
\]
推理演算¶
推理规则¶
-
全称量词消去规则
\[ (\forall x) P(x) \Rightarrow P(y) \]- 其中 \(y\) 是论域中一个体
- 意指如果所有的 \(x \in D\) 都具有性质 \(P\)，那么 \(D\) 中任一个体 \(y\) 必具有性质 \(P\)。
- 当 \(P(x)\) 中不再含有量词和其他变项时，这条规则明显成立。
- 而当允许 \(P(x)\) 中可出现量词和变项时，需限制 \(y\) 不在 \(P(x)\) 中约束出现(即右侧量不在左侧约束出现)。
- 设 \(P(x)＝ (\exists y)(x<y)\)，
- 则 \((\forall x)P(x)＝ (\forall x)((\exists y)(x<y))\) 在实数上成立
- 不应有 \((\forall x)P(x)⇒P(y)\)，因为 \(P(y)＝ (\exists y)(y<y)\) 是矛盾式。
- 这时，\(y\) 在 \(P(x)\) 中是约束出现了
- 全称量词引入规则
\[ P(y) \Rightarrow(\forall x) P(x) \]- 其中 \(y\) 是论域中任一个体
- 意指如果任一个体 \(y\)（自由变项）都具有性质 \(P\)，那么所有个体 \(x\) 都具有性质 \(P\)。
- 仍需限制 \(x\) 不在 \(P(y)\) 中约束出现(即右侧量不在左侧约束出现)
- 如 \(P(y)＝ (\exists x)(x>y)\) 在实数域上成立,
- \((\forall x)P(x)＝ (\forall x)((\exists x)(x>x))\) 是不成立的
- 存在量词消去规则
\[ (\exists x) P(x) \Rightarrow P(c) \]- 其中 \(c\) 是论域中的一个个体常项
- 意指如果论域中存在有个体具有性质 \(P\)，那么必有某个个体 \(c\) 具有性质 \(P\)。
- 需限制 \((\exists x)P(x)\) 中没有自由个体出现
- 如实数域上 \((\exists x)P(x) = (\exists x)(x>y)\) 是成立的， \(y\) 是自由个体，这时不能推导出 \(P(c)=c>y\)
- 还需限制 \(P(x)\) 中不含有 \(c\)。
- 如在实数域上 \((\exists x)P(x)=(\exists x)(c<x)\) 是成立的，\(P(c)=c<c\) 不成立
- 需限制 \((\exists x)P(x)\) 中没有自由个体出现
- 思考方式：先定 \(P\)， 再定 \(c\)， 最后讨论 \((\exists x)P(x)\Rightarrow P(c)\) 的正确性
- 存在量词引入规则
\[ P(c) \Rightarrow(\exists x) P(x) \]- 其中 \(c\) 是论域中一个个体常项
- 意指如果有个体常项 \(c\) 具有性质 \(P\)，那么 \((\exists x) P(x)\) 必真。
- 需限制 \(x\) 不出现在 \(P(c)\) 中。如实数域上， \(P(0) = (\exists x)(x>0)\) 成立，但 \((\exists x)P(x)=(\exists x)(\exists x)(x>x)\) 是不成立的。
推理演算¶
- 命题逻辑中引入推理规则的推理演算，可推广到谓词逻辑；
- 有关的推理规则（代入规则需补充说明）都可直接移入到谓词逻辑；
- 代入规则需补充说明：命题变项、自由个体变项和谓词变项的代入，要求保持合式公式和普遍有效性不被破坏
- 推理演算过程
- 以自然语句表示的推理问题引入谓词形式化
- 使用基本的推理公式
- 若不能直接使用基本的推理公式，则消去量词
- 在无量词下，使用规则和公式推理
- 引入量词以求得结论
谓词逻辑的归结推理法¶
归结证明过程¶
- 为证明 \(A \rightarrow B\) 是定理（\(A\)，\(B\) 为谓词公式），等价的是证明 \(A \wedge \neg B=G\) 是矛盾式，这是归结法的出发点
- 建立子句集 \(S\)
- 先将 \(G\) 化成等值的前束范式，进而将这前束形化成 Skolem 标准形（消去存在量词），得仅含全称量词的公式 \(G^{\prime}\)（曾指出 \(G\) 与 \(G^{\prime}\) 在不可满足的意义下是一致的）
- 再将 \(G^{\prime}\) 中的全称量词省略，\(G^{\prime}\) 母式（已合取范式化）中的合取词 \(\wedge\) 以“，”表示，便得 \(G\) 的子句集 \(S\)
- 而 \(S\) 与 \(G\) 是同时不可满足的，\(S\) 中的变元视作有全称量词作用着
-
对 \(S\) 作归结
-
设 \(C_{1}\)，\(C_{2}\) 是 \(S\) 中两个子句：
- 若 \(C_{1}\)， \(C_{2}\) 有互补对，消去互补对，得到新的归结式放入 \(S\) 中；
-
若 \(C_{1}\)， \(C_{2}\) 没有互补对，且它们无共同个体变元，不妨设 \(L_{1}\)，\(L_{2}\) 分别是 \(C_{1}\)，\(C_{2}\) 中的文字，如果 \(L_{1}\) 和 \(\neg L_{2}\) 有合一置换 \(\sigma\)，则
\[ \left(C_{1} \sigma-\left\{L_{1} \sigma\right\}\right) \cup\left(C_{2} \sigma-\left\{L_{2} \sigma\right\}\right) \]称作子句 \(C_{1}\)，\(C_{2}\) 的归结式
-
对子句集 \(S\) 的任两子句作归结（如果可作归结），并将归结式仍放入 \(S\) 中。
- 重复这过程直至归结出空子句 \(\square\)，得到矛盾，证明结束
-