最经典最简约的面向计算机科学的数理逻辑复习笔记.doc

该笔记适用于任何版本的数理逻辑！
绪论

一、数理逻辑研究什么？
★ 研究前提和结论的可推导性关系，它是由命题的逻辑形式而非内容所决定的

二、数理逻辑如何研究？
★ 形式语言

第一章 预备知识

第一节 集合

一、集合
1、 集合的内涵和外延（所有元素的共同性质/构成集合的所有元素）
2、 有序偶和笛卡儿集

二、关系
1、 概念：集合S上的n元关系R
2、 特殊情况：集合S上的一元关系R（集合S上的性质R）

三、函数（映射）
1、 概念：函数（集合＋有序偶＋性质）、定义域dom（f）、值域ran（f）
2、 概念：f（x）（函数f在x处的值）
3、 概念：f：S－>T（函数f是由S到T的映射）、满射、一一映射

四、等价
1、 概念：关系R是集合S上的等价关系（自反＋对称＋传递）
2、 概念：元素x的R等价类
3、 性质：R等价类对集合S的一个划分（两两不相交，且并为S）

五、基数
1、 概念：S～T（两个集合S和T是等势的）
2、 概念：集合S的基数|S|（集合中的元素个数）
3、 概念：可数无限集

第二节 归纳定义和归纳证明

一、归纳定义
1、 集合的归纳定义
⑴、直接生成某些元素
⑵、给出运算，将其作用在已有元素上，以产生新的元素
⑶、只有这样才是集合中的元素，除此之外，再也没有了
2、 典例：自然数集N的两个归纳定义

二、归纳证明
1、 归纳定理：设R是一个性质，如果
⑴、R（0）
⑵、对于任何n∈N，如果R（n），则R（n’）
那么，对于任何n∈N，都有R（n）
2、概念：归纳基础、归纳步骤（包括归纳变元和归纳假设）、归纳命题、归纳证明
3、概念：串值归纳法及其变形

三、递归定义
1、 递归定义（在归纳定义的集合上，定义函数）
在自然数集N上定义一个这样的函数f：g，h是N上的已知函数
f（0） ＝g（0）
f（n’）＝h（f（n））
2、 递归定义原理（这样的函数是存在而且唯一的）

第二章 经典命题逻辑

第一节 联结词

一、基本概念
1、 概念：命题（陈述句+确定值）（要么是真，要么是假）
2、 概念：简单命题和复合命题（区分的关键）
3、 小结：只考虑复合命题的真假是如何确定的

二、联结词
1、 非A：
2、 A与B：A为真并且B为真
3、 A或B：A为真或B为真（A为真或B为真或AB同时为真）
4、 A蕴涵B：如果A真，则B真（并非A假B真）
5、 A等值于B：如果A蕴涵B，同时B蕴涵A

第二节 命题语言

一、基本概念
1、 概念：命题语言（命题逻辑使用的形式语言）
2、 归纳：命题语言的三类符号（命题符号＋联结符号＋标点符号）
3、 概念：表达式、长度、空表达式、两个表达式相等
4、 概念：段、真段、初始段、结尾段

二、基本概念
1、 定义：原子公式，记为Atom（LP）（单独一个命题符号）
2、 定义：公式，记为Form（LP）（经典归纳定义及其两种变形）
★ 经典定义容易理解，然而两种变形更容易使用
3、 定理：如何证明LP的所有公式都满足R性质？
★ 关键：假设S={A∈Form（LP）| R（A）}
4、 概念：对公式的结构做归纳（上述归纳证明）

三、习题解析
1、 关键：利用二叉树表示公式的生成过程
2、 关键：蕴涵有多种不同的叙述方式（关键：分清楚充分条件和必要条件）
⑴、◆如果p，则q
⑵、◆只要p，则q
⑶、◆p仅当q
⑷、◆只有p，才q
⑸、◆除非p，否则q（思路：想方设法转化为上述情形）
第三节 公式的结构

一、引理
1、 引理1：LP的公式是非空的表达式
2、 引理2：在LP的每个公式中，左括号和右括号出现的数目相同
3、 引理3：真初始段不是公式（在LP的公式的任何非空的真初始段中，左括号出现的次数比右括号多。因此，LP的公式的非空的真初始段不是LP的公式（同理分析真结尾段））

二、定理
1、 定理：LP的每个公式恰好具有以下6种形式之一；并且在各种情形中，公式所具有的那种形式是唯一的
★ 注意：仔细分析其证明过程
2、 推论：LP的公式的生成过程是唯一的
3、 概念：否定式、合取式、析取式、蕴涵式、等值式

三、辖域
1、 概念：辖域、左辖域、右辖域
2、 定理：任何A中的任何辖域存在并且唯一
3、 性质：如果A是B中的段，则A中的任何联结符号在A中的辖域和它在B中的辖域是相同的
4、 定理：如果A是（¬B）的段，则A＝（¬B）或者A是B中的段；如果A是（B*C）中的段，则A＝（B*C）或者A是B或C中的段

四、其它
1、 算法：判断一个LP的表达式是不是公式的算法
2、 符号的省略：最外层括号＋其它形式的括号＋联结符号的优先级

五、习题解析
¬

第四节 语义

一、基本概念
1、 概念：真假赋值
2、 概念：公式的真假值AV（真假赋值v给公式A指派的真假值＋递归定义）
3、 定理：对于任何A∈Form（LP）和任何真假赋值V，AV∈{0，1}
★ 关键：如何证明LP的所有公式都满足R性质？

二、基本概念
1、 概念：∑V（∑表示公式集）
2、 概念：∑是可满足的（存在V，使得∑V＝1）
★ 注意：∑是可满足的蕴涵∑中的所有公式都是可满足的，但逆命题不成立
3、 概念：A是重言式、A是矛盾式
4、 概念：A的真假值表（真假赋值V给公式A指派的值，仅涉及V给A中出现的不同的命题符号所指派的值）
5、 性质：简化公式（熟练掌握简化公式）

三、习题解析
1、 性质：联结符号↔满足交换律和结合律
2、 性质：A是重言式，则A↔B是重言式当且仅当B是重言式

第五节 逻辑推论

一、逻辑推论
1、 符号：∑╞A（A是∑的逻辑推论，读作∑逻辑地蕴涵A）
2、 概念：∑╞A，当且仅当对于任何的逻辑赋值V，如果∑V＝1，则AV＝1
3、 概念：∑|≠A（存在逻辑赋值V，使得∑V＝1，AV＝0）
4、 特殊情况：Æ╞A（这时存在着性质：A是重言式）
5、 概念：逻辑等值公式A|＝|B
6、 例题分析：注意找到捷径和方法
⑴、如何证明一个逻辑推论是成立的（直接证明或者反证法）
⑵、如何证明一个逻辑推论是不成立的（构造出这样的真假赋值V，使得∑V＝1，AV＝0）

二、定理
1、 性质：合取符号和析取符号都满足交换律和结合律
2、 定理：
⑴、A1，…，An╞A，当且仅当Æ╞A1∧…∧An→A
⑵、A1，…，An╞A，当且仅当Æ╞A1→（…→（An→A）…）
3、 引理：如果A|＝|A’并且B|＝|B’，则有¬A|＝|¬A’等5条性质
4、 等值替换定理：设B|＝|C并且在A中把B的某些出现替换为C而得到A’，则A|＝|A’
5、 对偶性定理：A’|＝|¬A（其中A’是A的对偶）

第六节 形式推演

一、形式推演
1、 形式推演本质（形式推演仅涉及公式的结构，而与公式的语义无关）
2、 形式推演规则（共有11条规则）
3、 推论：如果A∈∑，则∑├A

二、形式可推演
1、 概念：形式可推演∑├A（∑├A，当且仅当存在有限序列∑1├A1，…∑n├An，其中的每一项∑k├Ak都是由使用某一形式推演规则生成，并且∑n＝∑，An＝A）
2、 概念的剖析：归纳定义

三、基础定理
1、 定理：如果∑├A，则存在有限的EO∈∑，使得∑O├A（对∑├A的结构做归纳）
2、 概念推广：∑├∑’（注意可以推广到无限情形）
3、 推演传递定理：如果∑├∑’，∑’├A，则∑├A

四、定理集群一（每一条都要求严格证明，并且反复记忆，作为后面证明的出发点）
1、 定理：（→定理群；定理2.6.4）
⑴、★★性质：A→B，A├B
⑵、★★性质：A→B，¬B├ ¬A
⑶、性质：A├B→A
⑷、性质：A→B，B→C ├A→C（蕴涵传递）
⑸、性质：A→（B→C）、A→B├A→C

2、 定理：（¬定理群；定理2.6.5）
⑴、★★性质：¬¬A├A；A├ ¬¬A
⑵、★★性质：如果∑，A├B；∑，A├ ¬B，则∑├ ¬A（归谬律，或称（¬＋））
⑶、性质：A，¬A├B

3、 定理：（→¬定理群之一；定理2.6.6）
⑴、★★性质：A→B├ ¬B→¬A（以此为基础衍生的4条性质）
⑵、★★性质：如果A├B，则¬B├ ¬A（以此为基础衍生的4条性质）
⑶、★★性质：A├B，当且仅当Φ├A→B（严格证明之）

4、 定理（→¬定理群之二；定理2.6.7）
⑴、性质：¬A→A├A（相似性质：A→¬A├ ¬A）
⑵、性质：A→B，A→¬B├ ¬A（相似性质：A→B，¬A→B├B）
⑶、性质：¬（A→B）├A（相似性质：¬（A→B）├ ¬B）

五、定理集群二（每一条都要求严格证明，并且反复记忆，作为后面证明的出发点）
1、 概念：语法等值公式A|－|B

2、 定理（∧定理群；定理2.6.8）
⑴、★★性质：A∧B|－|A，B
⑵、性质：A∧B|－| B∧A（∧交换律）
⑶、性质：（A∧B）∧C|－| A∧(B∧C)（∧结合律）
⑷、★★★★性质：¬（A∧B）|－| A→¬B（相似性质：¬（A→B）|－| A∧¬B）
⑸、性质：Æ├ ¬（A∧¬A）（不矛盾律）

3、 定理（∨定理群；定理2.6.9）
⑴、★★性质：A├A∨B，B∨A（最关键还是规则本身：允许在前面或后面增加∨）
⑵、性质：A∨B |－|B∨A（∨交换律）
⑶、性质：（A∨B）∨C|－| A∨(B∨C)（∨结合律）
⑷、★★★★性质：A∨B |－| ¬A→B（相似性质：¬A∨B |－| A→B）（分析其证明步骤）
⑸、★★性质：¬（A∨B）|－| ¬A∧¬B（Morgen定律）
⑹、★★性质：¬（A∧B）|－| ¬A∨¬B（Morgen定律）
⑺、性质：Æ├ A∨¬A（排中律）

4、 定理（∨∧定理群；定理2.6.10）
⑴、★★性质：A∨（B∧C）|－| (A∨B)∧（A∨C)（∨∧分配律）
⑵、★★性质：A∧（B∨C）|－| (A∧B)∨（A∧C)（∧∨分配律）
⑶、性质：A→（B∧C）|－| (A→B)∧（A→C)
⑷、性质：A→（B∨C）|－| (A→B)∨（A→C)
⑸、性质：（A→B）∧C|－| (A→C)∨（B→C)
⑹、性质：（A→B）∨C|－| (A→C)∧（B→C)

5、定理（↔定理群；定理2.6.11）
⑴、★★★★性质：A↔B|－|A→B，B→A（严格证明）
⑵、性质：A↔B|－| B↔A（↔交换律）
⑶、性质：A↔B|－|¬ A↔¬B
⑷、★★性质：¬（A↔B）|－| A↔¬B
⑸、★★性质：¬（A↔B）|－| ¬A↔B
⑹、性质：A↔B|－|（A∨¬B）∧（¬A∨B）
⑺、性质：A↔B|－|（A∧B）∨（¬A∧¬B）
⑻、性质：（A↔B）↔C|－|A↔( B↔A)（↔结合律）
⑼、性质：A↔B；B↔C├A↔C
⑽、性质：A↔¬A├B
⑾、性质：Æ├ （A↔B）∨¬（A↔¬B）

六、定理群
1、 定理：
⑴、A1，…，An├A，当且仅当Æ├A1∧…∧An→A
⑵、A1，…，An├A，当且仅当Æ├A1→（…→（An→A）…）
2、★★引理：如果A|－|A’并且B|－|B’，则有¬A|－|¬A’等5条性质
3、★★★★等值替换定理：如果B|－|C并且在A中把B的某些出现替换为C而得到A’，则A|－|A’
4、★★对偶性定理：A’|－|¬A（其中A’是A的对偶）

第七节 析取范式和合取范式

一、基本概念
1、 概念：单式（原子公式或者原子公司的否定式）
2、 概念：子式、析取子式、合取子式
3、 概念：析取范式、合取范式

二、定理
1、 定理：任何A∈Form（LP）逻辑等值于某一析取范式
2、 定理：任何A∈Form（LP）逻辑等值于某一合取范式

三、基本概念
1、 概念：公式A的析取范式（合取范式）
2、 概念：互补公式（一个公式和它的否定式，称为互补公式）
3、 定理：一个析取范式是矛盾式，当且仅当它的每个合取子式含互补的单式
一个合取范式是重言式，当且仅当它的每个析取子式含互补的单式
4、 定理：一个公式是矛盾式，当且仅当它的析取范式的每个合取子式含互补的单式
一个公式是矛盾式，当且仅当它的析取范式的每个合取子式含互补的单式
5、 概念：完全析取范式、完全合取范式

四、由公式导出它的析取范式（合取范式）的方法
1、 利用逻辑等值关系消去→、↔等符号（等值替换定理）
2、 利用逻辑等值关系进行化简

第八节 联结符号的完备集

一、基本概念
1、 概念：fA1…An（n元联结符号f，联结公式A1…An所构成的公式）
2、 性质：对于任何的n≥1，有2∧（2∧n）个不同的n元联结符号

二、基本概念
1、 概念：完备集（联结符号集称为完备的，当且仅当所有的n元联结符号都能由其中的联结符号定义）
2、 定理：{¬，∧，∨}是联结符号的完备集
3、 推论：{¬，∧}、{¬，∨}、{¬，→}是联结符号的完备集
4、 概念：↑称为与非式，即p↑q |=| ¬（p∧q）
5、 概念：↓称为或非式，即p↓q |=| ¬（p∨q）
6、 定理：{↑}，{↓}是联结符号的完备集

第三章 经典一阶逻辑

第一节 量词

一、基本概念
1、 概念：结构（论域＋个体＋关系＋函数）
2、 ★★概念：变元（以论域为变化范围的变元，用来构成关于个体的一般性命题或条件）

二、基本概念
1、 概念：全称量词和存在量词（对于所有（论域中的）个体：存在（论域中的）个体）
2、 概念：全称命题和存在命题（对于所有x，都有R（x）：存在x，使得R（x））

三、基本概念
1、 概念：命题函数（它不是命题，只有将某一个体指派为x的值时，它才成为命题）
2、 概念：自由变元、约束变元（命题函数中的变元、被量化的变元）
3、 归纳：量词的作用（将n元命题函数逐步转换为命题）

四、基本概念
1、 性质：论域D是有限集，可以将全称量词和存在量词，分别解释为合取和析取的推广
2、 概念：受限制的量词（范围受到限制的量词：范围由原来的论域，限制为论域的某个子集）
3、 性质：将受限制的量词，转换成为不受限制的量词（受限制的全称量词：全称量词＋蕴涵、受限制的存在量词：存在量词＋合取）
4、 概念：一阶逻辑和高阶逻辑（个体变元和个体量词/集的变元和量词）

第二节 一阶语言

一、基本概念：一阶语言的八类符号
1、个体符号：a、b、c
2、关系符号：F、G、H（n元关系符号、相等符号（特殊的二元关系符号））
3、函数符号：f、g、h（m元函数符号）
4、自由变元符号和约束变元符号（u、v、w和x、y、z）
5、联结符号（5类联结符号）
6、量词符号（全称量词符号∀、存在量词符号∃）（量词、全称量词、存在量词）
7、标点符号（左括号、右括号和标点）

二、基本概念：项
1、 概念： t∈Term（L），当且仅当它能由（有限次使用）以下的⑴、⑵生成：
⑴、a、u∈Term（L）（单独一个个体符号是项、单独一个自由变元符号是项）
⑵、如果t1，…tn∈Term（L），并且f是n元函数符号，则f（t1，…tn）是项
2、 概念：闭项（不含自由变元符号的项）
3、 概念：对项的结构作归纳（如何证明Term（L）中所有的元都具有某个性质）

三、基本概念：原子公式
1、 概念：L的表达式是Atom（L）中的元，当且仅当它有⑴、⑵两种形式之一
⑴、F（t1，…tn），其中F是n元关系符号，并且t1，…tn∈Term（L）
⑵、≡（t1，t2）（可以更直观的简写为：t1≡t2）
2、 注意：原子公式不是归纳定义

四、基本概念：公式
1、 概念：U（s1，…，sn） 表示符号s1，…，sn出现在表达式U中
2、 概念：A∈Form（L），当且仅当它能由（有限次使用）以下的⑴～⑷生成：
⑴、Atom（L）∈Form（L）
⑵、如果A∈Form（L），则（¬A）∈Form（L）
⑶、如果A、B∈Form（L），则（A*B）∈Form（L）
⑷、如果A（u）∈Form（L），x不在A（u）中出现，则∀xA（x），∃xA（x）∈Form（L）
3、 概念：闭公式（语句）（不含自由变元符号的公式）
4、 概念：拟公式（与公式结构相似的表达式、拟公式不是公式）
5、 概念：对公式的结构作归纳

五、定理群1
1、 定理1：L的任何项恰好具有以下三种形式之一：
2、 定理2：如果t是f（t1，…tn）的段，则t＝f（t1，…tn）或t是ti的段
3、 定理3：L的任何公式恰好具有以下八种形式之一：

六、定理群2
1、 概念：全称公式、存在公式（全称公式：∀xA（x），存在公式：∃xA（x））
2、 概念：量词的辖域（如果∀xA（x）是B的段，则称A（x）是∀x在B中的辖域）
3、 性质：量词的辖域是拟公式，联结符号如果出现在量词的辖域中，则可能是拟公式
4、 定理1：L的任何公式中任何全称量词或存在量词有唯一的辖域
5、 定理2：如果A是∀xB（x）中的段，则A＝∀xB（x）或是∀xB（x）的段

第三节 语义

一、基本概念：一阶语言的解释（后面五类符号，在所有一阶语言中都是相同的）
1、一阶语言和某个结构有联系（一阶语言是用来描述这个结构的）
2、一阶语言和任何结构无联系（一阶语言是一个一般的，抽象的一阶语言）
首先需要一个论域（只要求是不空的集合），然后再在该论域中如下解释：
⑴、个体符号解释为论域中的个体
⑵、n元关系符号解释为论域上的n元关系
⑶、m元函数符号解释为论域上的m元全函数
3、概念：全函数（处处有定义的函数，函数的运算结果不会跑到论域之外）

二、基本概念
1、 基本规定
⑴、项f（t1，…tn）被解释为论域中的个体：ƒ（a1，…an）
⑵、原子公式F（t1，…tn）被解释为命题：a1，…an有R关系
2、 系列结论
⑴、闭项和闭公式的解释（分别解释为论域中的个体，或命题）
⑵、含自由变元的项，经过解释（得到论域上的n元全函数）和指派，得到论域中的个体
⑶、对于一个含自由变元的公式，经过解释（得到命题函数）和指派，得到命题
3、 说明
⑴、区分：个体符号解释为个体，自由变元符号指派为个体
⑵、一次性指派：同时将所有的可数无限多个自由变元符号，指派为论域中的个体

三、基本概念
1、 概念：一阶语言L的赋值v（包括一个论域D和一个赋值函数v）
2、 概念：项的值（L的项在以D为论域的赋值v之下的值，递归定义如下）
3、 定理：设v是以D为论域的赋值，并且t∈Term（L），则tV∈D（对项的结构做归纳）

四、基本概念
1、 概念：定义一个新的赋值v（u/a）：它与原来的v处处相同，只是作用在自由变元符号u时，可能会不同
2、 概念：公式的真假值（L的公式在以D为论域的赋值v之下的真假值，递归定义如下）
⑴、取u不在A（x）中出现，由A（x）构作A（u）
⑵、∀xA（x）是由A（u）生成的，所以∀xA（x）V要由A（u）V来决定
⑶、∀xA（x）V＝1的涵义：无论v指派u为D中的哪一个个体a，都有A（u）V＝1
⑷、对于原来在A（x）中，现在仍在A（u）中的自由变元w来说，wV保持不变
★★归纳：如果v是∀xA（x）V中的指派，那么v（u/a）表示除此之外，还要给自由变元符号U作指派
3、定理：设v是以D为论域的赋值，A是公式，则AV∈{0，1}

五、基本概念
1、 概念：一致的（有相同论域的两个赋值v和v’，在四类符号上是一致的）
2、 定理：设v和v’是有相同论域的两个赋值，并且它们在项t和公式A所含的四类符号上都是一致的，则tV＝tV’，AV=AV’

六、基本概念
1、 概念：∑V（∑表示Form（L）中的公式集）
2、 概念：∑是可满足的（存在赋值v，使得∑V＝1）
3、 概念：A∈Form（L）是有效的（对于任何赋值v，都有∑V＝1）
4、 性质：可满足是由命题的内容决定的，而有效性是由公式的逻辑形式决定的
5、 性质：不存在一个统一的算法，用来判断L中公式的有效性或者可满足性

第四节 逻辑推论

一、逻辑推论
1、 符号：∑╞A（A是∑的逻辑推论，其中∑ÍForm（L），A∈Form（L））
2、 概念：∑╞A，当且仅当对于任何赋值V，如果∑V＝1，则AV＝1
3、 概念：∑|≠A（存在赋值V，使得∑V＝1，AV＝0）
★★前者是指任何论域上的任何赋值V，后者是指存在以D为论域的赋值V
4、 性质：Æ╞A（则A是有效公式）
5、 概念：逻辑等值公式A|＝|B

二、例题分析：注意找到捷径和方法
1、 如何证明一个逻辑推论是成立的（直接证明或者反证法）
2、 如何证明一个逻辑推论是不成立的（构造出这样的赋值V，使得∑V＝1，AV＝0）
⑴、性质：当确定赋值的论域时，问题在于论域的大小，和论域中有怎样的个体无关
⑵、D上的n元关系F：FV＝{<a1，…an>|a1∈D，…an∈D，且a1，…an满足F关系}

三、定理群
1、 引理1：如果A|＝|A’并且B|＝|B’，则有¬A|＝|¬A’等7条性质
2、 约定：B、C是拟公式，则B|=|C的含义是指B’|=|C’（注意B’、C’的形成）
3、 等值替换定理：设B|＝|C并且在A中把B的某些出现替换为C而得到A’，则A|＝|A’
（注意：B和C可能是拟公式）
4、 对偶性定理：A’|＝|¬A（其中A’是A的对偶）

第五节 形式推演

一、一阶逻辑的形式推演规则
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

第五节 一阶逻辑的完备性

一、存在性质
1、 概念：LO（在原先L的基础之上，增加新的可数无限多个自由变元符号）
2、 概念：∑ÍForm（LO），∑有存在性质（当且仅当对于Form（LO）中的任何存在公式
∃xA（x），如果∃xA（x）∈∑，则存在d使得A（d）∈∑）
3、 引理：极大扩充和存在性质（设∑ÍForm（L）并且∑是协调集，那么∑能扩充为极大
协调集∑*ÍForm（LO），并且∑*有存在性质）
★★证明步骤：由∑构作∑n（协调）→由∑n构作∑O（协调）→∑O扩充为极大协调∑*

二、一阶逻辑的完备性
1、 规定
⑴、首先：令论域T＝{ t’ | t∈Term（LO）}
⑵、然后：由∑*构作以T为论域的赋值v
2、 引理1：对于任何t∈Term（LO），tV＝t’∈T（对t的结构作归纳）
3、 引理2：对于任何A∈Term（LO），AV＝1当且仅当A∈∑*（对A的结构作归纳）

4、 可靠性定理：设∑ÍForm（L），A∈Form（L）
⑴、如果∑是协调的，则∑是可满足的
⑵、如果A是协调的，则A是可满足的

5、 可靠性定理：设∑ÍForm（L），A∈Form（L）
⑴、定理：如果∑╞A，则∑├A
⑵、推论：如果Æ╞A，则Æ├A

三、带相等符号的一阶逻辑的完备性
1、 首先：上面由∑*构作以T为论域的赋值v过程中，在由n元关系符号F确定FV时，如果关系符号是相等符号，则不再适用（即t1’＝t2’Ût1≡t2∈∑*不能保证）
2、 解决方案：
⑴、在Term（LO）定义二元关系R，t1Rt2Ût1≡t2∈∑*
⑵、依次证明：R是等价关系；用R将Term（LO）划分为等价类；以及构造出T*
⑶、由∑*构作以T*为论域的赋值v
⑷、最后分析：这样的处理避免了上面的矛盾

第六节 独立性

一、基本概念
1、 定义：形式推演系统中的某条规则是独立的（当且仅当它不能由其余的规则推出）
2、 证明（R）规则独立性的步骤
⑴、首先：构造出某条性质
⑵、其次：证明其余的规则，要么具有该性质，要么保存该性质
⑶、最后：由（R）规则构造公式∑├A，而它并不具有这个性质

二、证明形式推演系统各条规则的独立性
1、 规则（Ref）：
性质＝可以把∑改为Æ；公式＝F（u）├F（u）
2、 规则（＋）：
性质＝在∑├A中，前提至多含一个公式；公式＝A，B├A
3、 规则（¬－）：
改变赋值（¬A）V；性质＝如果∑├A，则∑╞A；公式＝¬¬A├A
推论：证明（¬＋）不能推出（¬－）
4、 规则（→＋）：
改变赋值（A→B）V；性质＝如果∑├A，则∑╞A；公式＝A├B→A
5、 规则（∀－）：
变换全称量词∀的辖域；性质＝变换以后规则仍然成立；公式＝∀xF（x）├F（u）
6、 规则（≡－）：
变换t1≡t2；性质＝变换以后规则仍然成立；公式＝F（u），u≡v├F（v）

第五章 紧致性定理、L-S定理、Herbrand定理

第一节 紧致性定理和L-S定理

1、紧致性定理：∑ÍForm（LO）可满足，当且仅当∑的任何有限子集可满足

2、L-S定理：
⑴、不含相等符号的∑可满足，当且仅当∑在可数无限论域中可满足
⑵、含相等符号的∑可满足，当且仅当∑在可数无限论域或某个有限论域中可满足

3、L-S定理的等价形式：利用有效性描述

第二节 Herbrand定理

一、基本概念
1、 概念：无∃前束范式（前束范式变换）
2、 变换步骤（分成两种情形处理：左边不出现全称量词＋左边出现全称量词）
3、 定理：前束范式A在论域D中可满足，当且仅当它的无∃前束范式在D中可满足
★★关键：不失一般性，假设A＝∃x∀y∃zB（x，y，z）

二、Herbrand定理
1、 概念：公式A的Herbrand域（以公式A中出现的3种符号所生成的项）
2、 概念：Herbrand赋值（以A的Herbrand域作为论域＋3类符号的赋值）
3、 定理：无∃前束范式A不可满足，当且仅当A在所有Herbrand赋值之下都取假值
★★关键：由v1构造Herbrand赋值v
4、 概念：母式的例式
5、 Herbrand定理：无∃前束范式不可满足，当且仅当存在有限个例式，它们不可满足

第六章 公理推演系统

第一节 公理推演系统

1、 区别：自然推演系统和公理推演系统
2、 公理推演系统的构成：公理＋规则（18条公理＋2条规则）
⑴、18条公理都是永真公式
⑵、2条规则的作用：如何由已有的永真公式，推演出新的永真公式
3、 定义：∑|－A（在公理推演系统中，A是由∑形式可推演性）当且仅当
有A1…An（＝A），其中Ak有4种可能
⑴、Ak是公理
⑵、Ak∈∑
⑶、Ak由前面两个公式使用R1生成
⑷、Ak由前面的A（u）（u不在∑中出现）使用R2生成

第二节 两种推演系统的关系

1、 引理：设∑