第五章 谓词逻辑的等值和推理演算¶
否定型等值式¶
-
若给定了两个谓词公式 \(A, B\)，说 \(A\) 和 \(B\) 是等值的，如果在公式 \(A, B\) 的任一解释下，\(A\) 和 \(B\) 都有相同的真值。
-
在谓词逻辑中， 需要给出解释的内容包括:
-
论域
-
谓词变项
-
命题变项
-
函数
-
自由个体
-
-
-
等价的说法:
-
\(A, B\) 等值当且仅当 \(A \leftrightarrow B\) 是普遍有效的公式
-
记作 \(A = B\) 或 \(A \iff B\)
-
由命题公式移植来的等值式¶
否定型等值式（摩根律的推广）¶
- 形式上看这对公式，是说否定词“\(\neg\)”可越过量词深入到量词的辖域内，但要把所越过的量词 \(\forall\) 转换为 \(\exists\)，\(\exists\) 转换为 \(\forall\)
量词分配等值式¶
量词对合取、析取的分配律¶
量词对蕴涵的分配律¶
全称量词对合取、存在量词对析取的分配律¶
变元易名后的分配律¶
范式¶
-
在命题逻辑里．每一公式都有与之等值的范式。
- 范式是一种统一的表达形式、当研究一个公式的特点(如永真、永假)时，范式起着重要的作用。
-
对谓词逻辑的公式来说也有范式
-
其中前束范式与原公式是等值的
-
其他范式与原公式只有较弱的关系
-
前束范式¶
-
前束范式：如果 \(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 标准形
-
基本推理公式¶
推理演算¶
推理规则¶
-
全称量词消去规则
\[ (\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\) 不成立
-
-
思考方式：先定 \(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\)，得到矛盾，证明结束