第五节 形式推演
一、一阶逻辑的形式推演规则 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
面向计算机科学的数理逻辑复习文档
![](/skin/haowen/images/icon_star.png)
![](/skin/haowen/images/icon_star.png)
![](/skin/haowen/images/icon_star.png)
![](/skin/haowen/images/icon_star.png)