第五节 形式推演
一、一阶逻辑的形式推演规则 1、 新增的形式推演规则（6条） 2、 规则的理解和分析
⑴、条件和结论的强弱：?xA（x）>A（t）>?xA（t） ⑵、u不在∑中出现：u表示的可以是论域中的任何一个个体 ⑶、区别：t比u的范围更广、代入和替换
3、 量词的形式推演规则的推广（只有t系列可以相同，也可以不同，u和x都不行） 4、 概念：∑├A（A是在一阶逻辑中，由∑形式可推演的），当且仅当∑├A能由（有限次使用）一阶逻辑的形式推演规则生成
二、定理群1
1、 定理1（定理3.5.2）
⑴、性质：?xA（x）|＝|?yA（y）（相似性质：?xA（x）|＝|?yA（y）） ⑵、性质：?x?y A（x，y）|＝|?y?x A（x，y）（相似性质：?x?yA（x，y）） ⑶、性质：?xA（x）├?xA（x）
⑷、性质：?x?y A（x，y）├?y?x A（x，y）
2、 定理2（?定理群，定理3.5.3） ⑴、性质：??xA（x）|＝|?x ?A（x） ⑵、性质：??xA（x）|＝|?x ?A（x）
三、定理群2
1、 定理（→定理群，定理3.5.4）
⑴、性质：?x[A（x）→B（x）] ├?xA（x）→?xB（x） 类似性质：?x[A（x）→B（x）] ├?xA（x）→?xB（x）
类似性质：?x[A（x）→B（x）] ，?x[B（x）→C（x）]├?x[A（x）→C（x）] ⑵、性质：A→?x B（x）|＝|?x[A→B（x）] 类似性质：A→?x B（x）|＝|?x[A→B（x）] ⑶、性质：?x A（x）→B|＝|?x[A→B（x）] 类似性质：?x A（x）→B|＝|?x[A→B（x）]
2、★★★★重要思路
⑴、当?出现在左边，使用?xA（x）├A（u）（?-） 当?出现在右边，使用规则（?+） ⑵、当?出现在左边，使用规则（?-）
当?出现在右边，使用反证法，或者规则（?＋）
四、定理群3
1、 定理1（∧定理群，定理3.5.5）
⑴、性质：A∧?x B（x）|＝|?x[A∧B（x）] 类似性质：A∧?x B（x）|＝|?x[A∧B（x）]
⑵、性质：?x[A（x）∧B（x）] |＝|?xA（x）∧?xB（x） 类似性质：?x[A（x）∧B（x）]├ ?xA（x）∧?xB（x） ⑶、性质：Q1A（x）∧Q2B（y）|＝|Q1Q2[A（x）∧B（y）]
2、 定理2（∨定理群，定理3.5.6）
⑴、关键：通过摩根定理，将∨转化为∧
⑵、最后一条性质：注意充分利用最开始的两条性质
3、 定理3（?定理群，定理3.5.7）（相对简单）
五、两个新的量词＋关于≡的两条规则 1、 概念：?!!x A（x）、?!x A（x）
⑴、分析：利用已有的两个量词定义出新的两个量词 ⑵、分析：解析公式＋详细涵义 2、 定理：
⑴、常规性质：≡的交换律、≡的传递律 ⑵、重要性质：?!x A（x）|＝|?xA（x），?!!x A（x）（分析其证明，曾经未能证明）
六、等值公式替换和对偶性
1、 引理：7条引理（5个常规联结符号＋2个量词符号） 2、 等值公式替换 3、 对偶定理
第六节 前束范式
一、基本概念
1、 概念：前束范式（Qx1…QxnB，其中B不再有量词） 2、 概念：前束词、母式
二、定理
1、 定理（约束变元符号替换）：将公式A中的?xB（x）的某些出现替换为?yB（y） 2、 定理：L的任何公式与某个前束范式等值（极其重要的8条公式） 3、 关键：将公式变换为前束范式的步骤（共三个步骤））
第四章 可靠性和完备性
第一节 可满足性和有效性
一、可满足性和有效性 1、 定理：（可满足和有效的相互转换）
⑴、性质：A是可满足的，当且仅当┐A是不有效的 ⑵、性质：A是有效的，当且仅当┐A是不可满足的
2、 定理（可满足和?、有效和?的相互转换）
⑴、性质：A（u1，…un）是可满足的，当且仅当?x1…?xn A（x1，…xn）是可满足的 ⑵、性质：A（u1，…un）是有效的，当且仅当?x1…?xn A（x1，…xn）是有效的
3、 定理（前束范式）
⑴、性质：A是可满足的，当且仅当A的前束范式是可满足的 ⑵、性质：A是有效的，当且仅当A的前束范式是有效的
二、在D中的可满足性和有效性
1、 定义：在D中的可满足性和有效性
⑴、∑在D中是可满足的（当且仅当有以D为论域的赋值v，使得∑V＝1） ⑵、A在D中是有效的（当且仅当对于任何以D为论域的赋值v，有AV＝1）
2、 性质：（可满足性变强了，有效性变弱了） ⑴、性质：∑在D中是可满足的?∑是可满足的 ⑵、性质：A是有效的? A在D中是有效的
三、论域变大变小的讨论
1、 定理（论域越大越满足，论域越小越有效） 设∑?Form（L），A∈Form（L），∑和A不含相等符号，D和D1是论域且|D|?|D1| ⑴、∑在D中是可满足的，则∑在D1中是可满足的 ⑵、A在D1中是有效的，则A在D中是有效的
2、 定理的证明
⑴、符号准备：以D-v构作D1-v1（关键：a’对应过去’，而b*对应回来） ⑵、引理1：以D1-v1构作D-v1*，则项t有这样的性质
⑶、引理2：同样以D1-v1构作D-v1*，则公式A有这样的性质
3、 重要反例（以证明上述定理不能含有相等符号，否则不成立）
第二节 可靠性
一、可靠性定理：设∑?Form（L），A∈Form（L） 1、 定理：如果∑├A，则∑╞A
2、 推论：如果?├A，则?╞A（若A是形式可证明的，则A是有效的）
二、性质
1、 性质：A（u）|≠?xA（x）；A（u）|≠?xA（x） 2、 推论：A（u）|＋?xA（x）；A（u）|＋?xA（x）
三、协调性
1、 定义：∑?Form（L）是协调的（当且仅当不存在A∈Form（L），使得∑├A且∑|?A）
2、 可靠性定理的协调性描述：设∑?Form（L），A∈Form（L） ⑴、定理：如果∑是可满足的，则∑是协调的 ⑵、推论：如果A是可满足的，则A是协调的 ★★两个定理和两个推论是两两等价的
3、 定理：∑?Form（L）是协调的，当且仅当存在A，使得∑|＋A
第三节 极大协调性
一、极大协调性
1、 定义：∑是极大协调的，当且仅当∑满足于以下的⑴和⑵ ⑴、∑是协调的
⑵、对于任何A≤∑，∑∪{A}不协调）
2、 定理：∑是极大协调的，则对于任何A，∑├A等价于A∈∑，∑|+A等价于A≤∑
二、∑封闭于形式推演
1、 定义：∑封闭于形式推演（如果对于任何A，∑├A蕴涵A∈∑） 2、 定理：设∑是极大协调的，则∑封闭于形式推演
三、定理
1、 定理：如果∑是极大协调的，则对于任何的A和B ⑴、?A∈∑， 当且仅当A≤∑
⑵、A∧B∈∑，当且仅当A∈∑且B∈∑等等
2、 Lindenbaum定理：任何协调的公式集能够扩充为极大协调集
★★关键：先由∑构造∑0、∑1、…∑n…，再令∑*＝∑0∪∑1∪…∪∑n…
第四节 命题逻辑的完备性
一、命题逻辑完备性的证明之一
1、 引理：设A∈Form（LP）含不同的原子公式p1，…pn，构作Ai，那么 ⑴、AV＝1?A1，…An├A ⑵、AV＝0?A1，…An├?A
★★证明：对公式A的结构作归纳
2、 定理：设A∈Form（LP），∑?Form（LP），并且∑是有限集 ⑴、如果?╞A，则?├A ⑵、如果∑╞A，则∑├A
★★证明：关键在于利用（pn∨?pn）→A├A
二、命题逻辑完备性的证明之二
1、 引理：设∑*是极大协调集，用∑*构作真假赋值v，使得对于任何的原子公式p pV＝1当且仅当p∈∑*，那么AV＝1当且仅当A∈∑*
2、 可靠性定理：设∑?Form（LP），A∈Form（LP） ⑴、如果∑是协调的，则∑是可满足的 ⑵、如果A是协调的，则A是可满足的
3、 可靠性定理：设∑?Form（LP），A∈Form（LP） ⑴、定理：如果∑╞A，则∑├A ⑵、推论：如果?╞A，则?├A
面向计算机科学的数理逻辑复习文档
