文章同步于@c.w.-知乎，个人博客
本文及其系列文章用于离散数学（1）科目的期末考试复习
由命题公式得来的等值公式
这部分我们把谓词逻辑看做命题逻辑中的命题变元，命题逻辑中正确的公式也是谓词逻辑中正确的公式。
例如，命题逻辑中，\(\neg\neg p=p\)是重言式，那么对于谓词逻辑\(\neg\neg (\forall x)P(x)=(\forall x)P(x)\)是一个有效式。
这部分是谓词逻辑的一个重要基石，因为谓词逻辑中很多细节性的、不涉及量词变换的等值公式都是由此得来的。
否定型等值式⭐⭐
这部分是最最重要的基础。
-
\(\neg(\forall x)P(x)=(\exists x)\neg P(x)\)
-
\(\neg(\exists x)P(x)=(\forall x)\neg P(x)\)
可以这样直观的理解和解释：
-
并不是对于所有的\(x,P(x)\)都成立，那么肯定存在一个\(x,P(x)\)不成立，即\(\neg P(x)\)成立。
-
不存在一个\(x\)让\(P(x)\)成立，那么对于所有的\(x,P(x)\)都不成立，即\(\neg P(x)\)成立。
谓词公式和命题变项的分配律
有关\(\land\)和\(\lor\)的分配律⭐
-
\((\forall x)(P(x)\land q)=(\forall x)P(x)\land q\)
-
\((\forall x)(P(x)\lor q)=(\forall x)P(x)\lor q\)
-
\((\exists x)(P(x)\land q)=(\exists x)P(x)\land q\)
-
\((\exists x)(P(x)\lor q)=(\exists x)P(x)\lor q\)
这部分是比较好理解的，也是非常基础性的定律。
有关\(\rightarrow\)的分配律
-
\((\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)(q\rightarrow P(x))=q \rightarrow (\forall x)P(x)\)
-
\((\exists x)(q\rightarrow P(x))=q \rightarrow (\exists x)P(x)\)
注意到前两个式子变化后量词发生了改变。证明如下（只证第一个，其余同理）
\((\forall x)(P(x)\rightarrow q)\\\\=(\forall x)(\neg P(x)\lor q)\\\\=(\forall x)\neg P(x)\lor q\\\\=\neg (\exists x)P(x)\lor q\\\\=(\exists x)P(x)\rightarrow q\)
可以发现还是运用了\(P\rightarrow Q=\neg P\lor Q\)这个重要的式子。
谓词公式的分配律
变量不易名
-
\((\forall x)(P(x)\land Q(x))=(\forall x)P(x)\land (\forall x)Q(x)\)⭐
-
\((\exists x)(P(x)\lor Q(x))=(\exists x)P(x)\lor (\exists x)Q(x)\)⭐
注意，这两处是等号。可以这样理解：
-
如果对于所有的\(x\)，\(P(x)\land Q(x)\)成立，那么对于所有的\(x,P(x)\)成立,并且对于所有的\(x,Q(x)\)成立。而且容易发现这是充要的。
-
如果存在一个\(x\)，使得对于这个x而言，\(P(x)\)或者\(Q(x)\)成立，那么对于\(P(x)\)和\(Q(x)\)本身而言，肯定存在一个\(x\)让\(P(x)\)成立或者存在一个\(x\)让\(Q(x)\)成立。而且容易发现这是充要的。
下面是两个推导的符号。注意，不是等号！
-
\((\forall x)P(x)\lor(\forall x)Q(x)\Rightarrow(\forall x)(P(x)\lor Q(x))\) ⭐
-
\((\exists x)(P(x)\land Q(x))\Rightarrow (\exists x)P(x)\land (\exists x)Q(x)\) ⭐
可以这样理解
-
如果\(P(x)\)对于所有的\(x\)成立或者\(Q(x)\)对于所有的x成立，那么对于所有的\(x\),一定有\(P(x)\)或者\(Q(x)\)成立。但是如果对于所有的\(x\)有\(P(x)\)或者\(Q(x)\)成立，那么考虑如下情况：对于一半的\(x\)是\(P(x)\)成立但是对于另一半是\(Q(x)\)成立，\((\forall x)P(x)\)和\((\forall x)Q(x)\)就都不成立。
-
如果存在一个\(x\)，使得这个\(x\)既让\(P(x)\)成立又让\(Q(x)\)成立，那么仍旧取这个\(x\)，\((\exists x)P(x)\)和\((\exists x)Q(x)\)都成立。但是如果\((\exists x)P(x)\)成立且\((\exists x)Q(x)\)成立，那么考虑如下情况：对于\(x_1\)而言\(P(x_1)\)成立而\(Q(x_1)\)不成立，对于另一个\(x_2\)而言\(P(x_2)\)不成立而\(Q(x_2)\)成立，对于其余的个体词，\(P(x)\)和\(Q(x)\)都不成立，那么很明显\((\exists x)P(x)\)成立且\((\exists x)Q(x)\)成立，并且不存在某个\(x_0\)让\(P(x_0)\)和\(Q(x_0)\)同时成立。
变量易名
-
\((\forall x)(\forall y)(P(x)\lor Q(y))=(\forall x)P(x)\lor(\forall x)Q(x)\)
-
\((\exists x)(\exists y)(P(x)\land Q(y))=(\exists x)P(x)\land(\exists x)Q(x)\)
变量易名主要目的是为了化简式子，减少或者增加式子中的变元。
注意，下列式子仍旧是推导的符号而不是等值的式子。
-
\((\forall x)(\forall y)(P(x)\lor Q(y))\Rightarrow(\forall x)(P(x)\lor Q(x))\)
-
\((\exists x)(P(x)\land Q(x))\Rightarrow(\exists x)(\exists y)(P(x)\land Q(y))\)
证明和理解方式可以参考上一小节。
范式
前束范式
- 对于一个公式\(\varphi\)，如果其所有的量词都位于这个公式的最左边（不含否定词），并且这些量词的辖域都延伸到公式的最末端，那么称之为前束范式。
求前束范式的步骤就是反复运用上面提到的分配律把所有的量词一步一步提到最前面。
例1：求\(\neg((\forall x)(\exists y)P(a,x,y)\rightarrow (\exists x)(\neg(\forall y)Q(y,b)\rightarrow R(x)))\)的前束范式
原式\(\\\\=\neg(\neg((\forall x)(\exists y)P(a,x,y))\lor(\exists x)((\forall y)Q(y,b)\lor R(x)))(把所有联结词转换为与或非)\\\\=(\forall x)(\exists y)P(a,x,y)\land\neg (\exists x)((\forall y)Q(y,b)\lor R(x))\\\\=(\forall x)(\exists y)P(a,x,y)\land(\forall x)((\exists y)\neg Q(y,b)\land\neg R(x))(把所有\neg 内移)\\\\=(\forall x)((\exists y)P(a,x,y)\land (\exists y)\neg Q(y,b)\land\neg R(x))(量词左移)\\\\=(\forall x)((\exists y)P(a,x,y)\land (\exists z)\neg Q(z,b)\land\neg R(x))(变元易名)\\\\=(\forall x)(\exists y)(\exists z)(P(a,x,y)\land \neg Q(z,b)\land\neg R(x))(量词左移)\\\\=(\forall x)(\exists y)(\exists z)S(a,b,x,y,z)\)
其中，最后的\(S(a,b,x,y,z)\)是原公式的母式。
Skolem标准形
- Skolem标准型就是只保留了全称量词的前束范式。
求skolem标准型的步骤，就是在把式子化为前束范式的基础上消去式子中的存在量词。具体步骤为：
- 从左至右依次检查每个量词。如果一个这个量词是全称量词，那么跳过。如果这是一个存在量词，那么检查这个量词前面是否有全称量词。如果没有，那么在前束范式中用论域中的某个常元替代所有这个变元，然后删去这个存在量词；如果有，那么设其前面出现的全称量词作用的变元为\(x_1,x_2,……,x_m\)，在前束范式中用一个关于\(x_1,x_2,……,x_m\)的函数\(f(x_1,x_2,……,x_m)\)替代所有这个变元，然后删去这个存在量词。
例2：求\((\exists x)(\forall y)(\forall z)(\exists u)(\forall v)(\exists w)P(x,y,z,u,v,w)\)的Skolem标准形。
第一个量词为\((\exists x)\)，前面无其余全称量词，用某一常项\(a\)替代\(x\)，删去\((\exists x)\)，得到\((\forall y)(\forall z)(\exists u)(\forall v)(\exists w)P(a,y,z,u,v,w)\\\\\)随后的两个量词为\((\forall y)(\forall z)\)，是全称量词，跳过。\(\\\\\)接下来的量词为\((\exists u)\)，前面有\((\forall y)(\forall z)\)，所以用一个和\(y,z\)有关的函数\(f(y,x)\)来替换\(u\)，并删去\((\exists u)\)，得到\((\forall y)(\forall z)(\forall v)(\exists w)P(a,y,z,f(y,x),v,w)\\\\\)接下来的量词是\((\forall v)\)，跳过。\(\\\\\)最后一个量词为\((\exists w)\)，前面有\((\forall y)(\forall z)(\forall v)\)，用一个和\(y,z,v\)有关的函数\(g(y,z,v)\)替代\(w\)，并删去\((\exists w)\)，得到最终的结果：\((\forall y)(\forall z)(\forall v)P(a,y,z,f(y,x),v,g(y,z,v))\)
