北邮高级数理逻辑课件.doc

形式系统
形式系统由{∑, TERM, FORMULA, AXIOM, RULE}等5个部分构成，其中 称为符号表，TERM为项集；FORUMULA为公式集；AIXIOM为公理集；RULE为推理规则集。：
1、 符号表∑为非空集合，其元素称为符号。
2、 设∑为∑上全体字的组合构成的集合。项集TERM为∑的子集，其元素称为项；项集TERM有子集VARIABLE称为变量集合，其元素称为变量。F(X) a, X,
3、 设∑为∑上全体字的组合构成的集合。公式结FORMULA为∑的子集，其元素称为公式；公式集有子集ATOM，其元素称为原子公式。 A(f(a,x1,y)), AàB
4、 公理集AXIOM是公式集FROMULA的子集，其元素称为公理。
5、 推理规则集RULE是公式集FORMULA上的n元关系集合，即RULE=，其元素称为形式系统的推理规则。
其中公式集和项集之间没有交叉，即TERM∩FORMULA =φ，公式和项统称为表达式。

由定义可知，符号表∑、项集TERM、公式集FORMULA是形式系统的语言部分。而公理集AXIOM、推理规则集RULE为推理部分

形式系统特性
1、 符号表∑为非空、可数集合（有穷、无穷都可以）。
2、 项集TERM、公式集FORMULA、公理集AXIOM和推理规则集RULE是递归集合，即必须存在一个算法能够判定给定符号串是否属于集合（可判定的）。
3、 形式系统中的项是用来描述研究的对象，或者称为客观世界的。而公式是用来描述这些研究对象的性质的。这个语言被称为对象语言。定义公式和项产生方法的规则称为词法。
公理：
I
II
III
证明：AàA
(1)
Aà(AàA)
((Aà(BàC))à((AàB)à(AàC))
((Aà(BàA))à((AàB)à(AàA))
((Aà((AàA)àA))à((Aà(AàA))à(AàA))
Aà((AàA)àA))
(Aà(AàA))à(AàA)
(Aà(AàA))
AàA
分离规则

已知：R是一个有关公式的性质
证明：R对于所有公式有效
I. 对于，则
II. 假设公式A和B都具有R
III. ，且，则
IV. 是公式，如果且，则
根据：形式系统的联结词只有两个，因为在命题逻辑的语义上，其他联结词可以有这两个联结词表示。
已知：
求证：A成立
(1)
A是公式

(2)
{，}├
{，}├
├
反证
(3)

3

公理代入原理：设A(P)为含有变元P的公理（定理同样适用），如果将公式A中的变元P替换为命题变元B，则A(B)仍为公理（定理）；（公理填充）
等价替换原理：设命题公式A含有子公式C（C为命题公式），如果C├│D，那么将A中子公式C提换为命题公式D（不一定全部），所得公式B满足A├│B。
紧致性：设为FSPC上的公式集合，A为FSPC的公式。如果├，则存在的有限子集0 使得0 ├。
已知：Aà(BàC), B
证明：AàC
公理推演：
Aà(BàC)
A
BàC
B
C
自然推演：
f(B)=1,f(A)=0或者f(BàC)=1。
假设f(A)=0;则f(AàC)=1.
假设f(A)=1,那么f(BàC)=1.f(B)=1,则f(C)=1.因此，f(AàC)=1.
由此，命题成立。
给出一个形式系统，其公理定义如下：
{A, (,), à,}
{}
{---}

给出公理如下：
AàA
AàAàA
(AàA)à(AàA)
(AàA)à(AàA)
(A-->A-->A)-->(A-->A)
下列哪些是定理？
AàAà(AàA)
(AàA)à(AàA)à(AàA)
(AàAàA)à(AàAàA)
(AàB)à(AàB)à(AàB)
语义构成
结构：（有两个主要部分构成）
*确定研究对象集合，论域或个体域
*把形式系统中的变量到论域中的一组规则映射规则
域值：指一组给公式赋值的规则
根据这项规则将 －AtomicValue中
语义的特殊公式
1) 公式A为永真式，重言式tautologies，如果对一切赋值，.
2) 公式A为永假式，矛盾式contradictions,如果对一切赋值，
3) A，B为逻辑等价的，如果对于一切赋值，，记做A╞B(A|=|B)
4) 公式A为可满足的，如果至少存在一个赋值，
逻辑推论：设是一个FSPC上的公式集合，A是FSPC上的任一公式。A为的逻辑结果，记做|=A，当且仅当对任何赋值映射v，如果＝1时，则。|=读作逻辑蕴涵。
逻辑等价：设公式A和公式B分别为FSPC上的两个公式。A和B为逻辑等价的，记做A|=|B当且仅当A|=B和B|=A同时成立。
永真式：如果A为永真式，则公式集合为空集，即|=A。
演绎定理：
设为FSPC的公式集合，A和B分别为FSPC上的公式。|=成立的充分必要条件是：|=。
证明：
从语义上：
必要性：
由于f1()=1，则f1(AàB)=1;
由于f1(AàB)=1,并且f1(A)=1，则f(B)=1

充分性：
对于映射f，若f()=1，
假设f1(A)=0;f1(AàB)=1.
假设f1(A)=1, 由于已知条件可以知道f(B)=1.因此，f(AàB)=1

从形式上：
必要性：
＝1成立，则成立。
对于成立有两种情况，为了证明╞成立，只需考虑，使＝1的情况。
如果赋值映射v，满足＝1，＝1且，则有＝1。因此，╞成立。

充分性：
任取赋值映射v，满足，则有：
当＝0时，有╞
当＝1时，由已知＝1， 因此╞
联结词的完备集：联结词的集合为完备的，当且仅当对于其他的联结词都可以由这个联结词的集合中的元素来表示。
FSPC中的完备集：、、、、等。如果引入异或，那么异或与也构成一个完备集合。
形式化系统à语义结构à元理论à自动化

语法构成
语法构成研究形式系统语言构成规律。主要研究推演（重写）规律；主要规律：
（1）独立性：如果形式系统中每一个公理都是独立的，即把任一公里A从形式系统中删除后，所得形式系统FSˊ不满足├FS′A（即A不是FSˊ的定理），则称形式系统为独立的；
l 独立形式系统是简洁的；
（2）一致性：形式系统FS称为一致性，或相容的（consistent）如果不存在FS的公式A，使得├A，├同时成立；
l 所有形式系统都应该是一致的；
（3）完全性：形式系统为完全的，如果对形式系统中任意公式A，或者├A成立，或者├成立；
l 完全性的形式系统，一切都是可知的；因此，几乎没有价值；
（4）可判定性：形式系统FS称为可判定的，如果存在一个算法，对FS对的任一公式A，可确定├A是否成立，否则称FS是可判定的；如果上述算法对定理能作出判断，而对于非定理未必终止（作判断），称FS为半可判定的；
l FS为可判定的，当且仅当定理集合为递归集；
（5）公式集合一致性：称形式系统的公式集合为一致的，如果形式系统是一致的，且不存在公式A使，├A ，├ 同时成立。

语法和语义关系
合理性（soundness）：称形式系统FS是合理的，FS的任意公式A有：├FS，则|=M，M为所有结构；
完备性（Completeness）：称形式系统FS是完备的，如果对FS的任意公式有：若|=M，则├FS，这里M为FS所讨论的一类结构；
紧致性：称形式系FS是紧致的，如果对FS的任意公式集有：如果公式集的所有穷子集是可满足的，那么公式集也是可满足的；

合理性证明：
已知：A是定理
求证：A是永真的

由于A是定理，存在一个证明序列A1,A2,……An=A。
N=1时：A1=A。由于A1或者为公理或者是前边的公式通过推理规则得到。因此，A1是公理，也就是A是公理。对于任意的赋值映射f，则f(A)=1。
假设：n<m时，命题成立：A是定理则A是永真的。
证明：当n=m时，命题成立。
A1,A2,……Am-1, Am=A v
1, Am是公理：公理是永真的，因此命题成立。
2, Am是前边通过推理规则得到的。推理分离规则，三段论。假设Am是由Ai和Aj通过分离规则得到。由于归纳假设，Ai和Aj都是永真的。由于推理规则保真性，那么Am是永真的。因此，命题成立。

自由变元：自由变元是真正的变元，可以将个体域中的任意个体代入到自由变元中。类似于数学中的变元。
约束变元：约束变元并不是实际意义的变元（数学意义上的变元）。约束变元是为表达某种想的辅助符号。

自由变元 约束变元
可代入 不可代入
不可改名 可改名

量词中的变元成为指导变元，指导 4变元是约束变元

改名原理：在FSFC中，称公式A´为公式A的改名式，如果将A中至少一个量词的指导变元和相应的约束变元（如果有）都改为另一个相同名字的变元后得到的公式A’。在FSFC中，如果A’为公式A的改命式，且A’改用的变元在A中无任何出现，那么A├│A’。

量词规则
全称（）消去规则：如果├，且项t对于公式为可代入的，则├。
全称（）引入规则：如果├，t不在中出现，则├。
存在（）销去规则：设为FSFC的任意公式集合，A, B为公式。变元x在和公式B中无出现。如果├，├则├B。
存在（）引入规则：设为FSFC的任意公式集合，B为公式。变元x在和公式B中无出现。如果├B，则├。

形式语义基本概念
1、 指称语义：语义是由语义结构和以及在这种结构下公式赋真值的规定构成的。
2、 语义结构：对于抽象公理系统或形式系统作出的一种解释。包括个体域和在这种个体域上的个体运算和个体间关系。
下面给出形式系统语义的定义：
3、 形式语义：设FS是已经存在的形式系统，FS的语义有语义结构和赋值两个部分组成：
a) 语义结构：当FS的项集TERM不为空时，由非空集合U和规则组I所组成二元组（U，I），称为形式系统FS的语义结构。其中U和I的性质如下：
i. U为非空集合，称为论域或者个体域；
ii. 规则组I，称为解释，根据规则组的规定对项集TERM中的成员指称到U中的个体；规定对原子公式如何指称到U中的个体性质（U的子集）、关系（的子集）。
b) 指派：若形式系统FS中的变量集合Variables非空，那么下列映射称为指派：
s：varibles－>U。
对于给定的语义结构，可以将指派扩展到项集TERM上：
：TERM－>U；
＝S(t) 当t 为变元
S指派t中变元由解释确定 当t为非变元
c) 赋值：是指一组给公式赋值的规则，据此规则可对每一结构U和指派S确定一由原子公式到值域的映射v：atomic－>value。根据这个赋值规则，可以将赋值映射进行扩展：v为：
d) 可满足：公式A称为可满足，如果存在结构S与指派s，使一个赋值映射v满足v(A)=1,否则为不可满足。

一阶谓词语义
1、语义结构：
一阶谓词形式系统采用TARSKI语义结构。这种语义结构以为其真值集合。每一个Tarski语义结构S，由非空集合U和下列解释I构成：
1. 常元：对于任一常元a, I(a)U, I(a)记为，为论域中的一个元素；
2. 函数： 对于任一n元函数为U的一个n元函数，记为：；
3. 谓词：对于任一n元谓词，为U上的一个n元关系，记为，。当n=1时，为U的子集。
2、指派：
指派S为变元集合到上的映射。S可以扩展为：
对于每一变元v：；
对于每一常元a：；
对于每一个n元函词fn和项t1，t2…….tn：

由此可见，指派与结构无关，而与结构相关。
3、赋值：
i． 赋值映射v：Atomicà定义为：对任何n元谓词及项t1……tn，当且仅当<>，其中。
ii． 赋值映射v按下列规则扩展，：
对原子公式A：；
对于公式，当且仅当；
对于公式，当且仅当或；
对公式，当且仅当对于U中每一元素d， ，其中表示指派S对x指派元素d。
已知：任意取一个结构,一个赋值映射f，f满足f()=1：
证明：f()=1.
设x取值为d
f((AàB)(d))=1
f(A(d)àB(d))=1;
f(A)(d)=1
f(B(d))=1
对于论域中的任意一个个体，d, f(A(d)àB(d))=1, f(A(d))=1,
f(B(d))=1

一阶谓词形式系统的语义结构：只有一个函词、一个谓词和一个常元的形式系统（推理和符号与一阶谓词相同）。
个体域：，即自然数集合N
谓词：为N上的关系。
函词：为N上的后继，即
常元：

判断以下公式的真值：
=1
=1
=0

形式逻辑基本发展思路
推理过程：
语义
逻辑推理
反证，真值表
合理、完备
公式
形式系统
公理，规则（分离规则）（机器难以识别）
同可满足
标准形式
标准形式
＋，－，代替（机械化）
为什么同可满足？

skolem标准形
设公式A为前束范式（其母式为析取范式和合取范式）。称为A的斯柯伦标准形，如果是用skolem常元、skolem函词消除A中量词后得到的公式。当A的母式为合取范式时，其斯柯伦标准形称为合取型，否则称为析取型。斯柯伦标准型通常的约定为合取型。
例：求公式的斯柯伦标准型。

求一个公式a的Skolem标准型的算法：
１°.先将a化为前束范式b1:=Qx1⋯QxnA，其中A为母式，不含量词。若所有的Qi:="(1£ i £n)，则b1显然是Skoloem标准型。取b:=b1 ，即为所求。算法结束;否则转2° ：
　　2°.若b1形为$x1 "x2⋯"xn A，则选一不在A中出现的个体常项c(称为Skolem常项),可得
b2:="x2⋯"xn
显然b2是一Skolem标准型。取b :=b2 ，即为所求。算法结束;
３°.若b1形为"x1⋯"xk$xk+1Qk+2xk+2⋯QnxnA，则选一不在A中出现的k元函词符号f(称为Skoloem函词)，可得
b2:="x1…"xkQk+2xk+2⋯Qnxn
若Qk+2 ,⋯, Qn全为"，则显然b2是一Skolem标准型。取b :=b2 ，即为所求。算法结束;
否则返回到３°自己。

子句集概念
对于合取型斯柯伦标准型，其合取项被称为子句，其析取项被称为文字。
由于每个合取型斯柯伦标准型，有多个子句构成。我们可以把一个斯柯伦标准型中的所有子句集合在一起。这样一个斯柯伦标准型，就有了一个与其对应的等价的子句的集合。
公式àSkolem AàC1&C2&C3={C1,C2,C3}::C1=L1vL2vL3.....
公式集合S被称为公式A的子句集，如果S为A的斯柯伦标准型中全体子句的集合。S称为可满足的，如果存在一个结构使S中的每个子句为真；否则称子句集合为不可满足的。

公式à前束范式àSkolem标准型à子句集

子句集性质
（1） 子句集中两个子句中变量是独立的、无关的，不管子句中的变量名称是否相同。这主要是因为：。同一子句中的变量是相互依赖的。
（2） 斯柯伦标准型与源公式之间是同可满足的，斯柯伦标准型与子句集之间是等价的。因此，子句集与原公式之间是同可满足的。
（3） 如果子句集是可满足的，则子句集的子集都是可满足的。相反，如果一个子句集的子集是不可满足的，则子句集是不可满足的。

求子句集
通常通过以下步骤，可以得到一个公式的子句集。
1.求A的合取型前束范式
2.求A的skolem标准形
3.求skolem的析取范式
4.将skolem析取范式改为子句

例：求公式的子句集。
"x$y($z(~P(x,y) Q(x,z)) $zR(x,y,z))
"x$y$z((~P(x,y) Q(x,z)) R(x,y,z))
"x$y$z((R(x,y,z) ~P(x,y)) (Q(x,z)) R(x,y,z)))
"x$z((R(x,f1(x),z) ~P(x,f1(x))) (Q(x,z)) R(x,f1(x),z)))
"x((R(x,f1(x),f2(x)) ~P(x,f1(x))) (Q(x,f2(x))) R(x,f1(x),f2(x))))
(R(x,f1(x),f2(x)) ~P(x,f1(x))) (Q(x,f2(x))) R(x,f1(x),f2(x)))

子句集为：
{R(x,f1(x),f2(x)) ~P(x,f1(x))， Q(x,f2(x))) R(x,f1(x),f2(x))}

前束范式

合取范式

skolem标准型
子句集
子句1
子句2

二元归结：为分别为FSPC中，含有互补文字的子句，L1= L2那么下面推理称为二元归结：
C1 , C2

其中，称C1 , C2为归结母式，为归结结果，L1L2为归结基。

已知：C为C1和C2的归结结果，
求证：C为的逻辑结果。
C=
C1=(C1-L1)vL1
C2=(C2-L2)VL2
f(C1)=1，f(C2)=1
f(L1)=1,则f(L2)=0
f(L1)=0,则f(L2)=1
f(c)=f(C1-L1)v f(C2-L2)
C1=(c1-l1)vL1
f(l1)=0, f(c1-l1)=1 因此，f(c)=1
f(l1)=1，f(l2)=0，则f(c2-l2)=1，f(c2)=f(c2-l2)Vf(l2)
f(c)=1

代换需要注意的是：
首先代换不能是自身代换，用同一变量代换本身是没有什么意义的；
其次，对于代换的过程是一次性将所有的变量同时代换成项，而不是先代换第一项，再代换第二项的顺序结构。

设公式为，代换为，求代换结果。
：{f(y)/x}O{z/y}，同时代换
结果：P(f(y),z,z)

{f(y)/x}*{z/y}，先进性前一项代换，再进行后一项代换
,==
结果：P(f(z),z,z)

合一
既然有了代换的概念，我们必然要考虑，能够将一些不同公式通过代换化为一个公式。合一就是用来解决这样的问题。代换称为表达式集合的合一，如果；当表达式集合有合一时，称为集合时可合一的。

Herbrand域：集合H称为子句集S的Herbrand域，如果 ，其中Hi递归定义如下：

其中a为任意常元。

P(f(x),g(y)) ;
H0={a},
H1={a,f(a),g(a)}
H2={a,f(a),g(a),f(f(a)),f(g(a)) g(g(a)),g(f(a)),}
….

Herbrand定理
l 子句集S为不可满足的，当且仅当S对所有Herbrand解释都是不可满足的。
l Herbrand定理：子句集S为不可满足的，当且仅当S的基例的有穷集合是不可满足的。

例：子句集：

显然为可满足的。

显然是不可满足的。
由于找到一个是不可满足的，因此，子句集S是不可满足的。

练习，利用归结原理证明，以下的子句集是不可满足的。

(8) ~E(x)Vv(x)V~p(f(x))
(9) ~E(a)Vv(a)Vp(f(x))
(10) v(a)Vp(f(a))
(11) v(a)V~p(f(a))
(12) ~v(a)
(13) p(f(a))
(14) ~p(f(a))
(15) 空子句

练习
给定有向图，令谓词表示节点为可达的；用表示节点可达蕴涵节点可达（即从节点到节点有有向边）。请建立HORN子句程序，并证明：由节点可达节点。

ßGo(Z)
Go(A)ß
Go(B)ßGo(A)
Go(E)ßGo(B)
Go(X)ßGo(E)
Go(Z)ßGo(X)
ßGo(X)
ßGo(E)
ßGo(B)
ßGo(A)
口
注：右边起点（可达），左边终点（想达到