第五节 一阶逻辑的完备性
一、存在性质
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、 引理：设∑?Form（L），A∈Form（L），如果∑|－A，则∑├A 2、 引理：设∑?Form（L），A∈Form（L），如果∑├A，则∑|－A
★★注意：可以使用推演定理（如果∑，A|－B，则∑|－A→B）作为证明基础 3、 定理：设∑?Form（L），A∈Form（L），∑├A当且仅当∑|－A