《高级数理逻辑第5讲.doc》由会员分享，可在线阅读，更多相关《高级数理逻辑第5讲.doc（15页珍藏版）》请在taowenge.com淘文阁网|工程机械CAD图纸|机械工程制图|CAD装配图下载|SolidWorks_CaTia_CAD_UG_PROE_设计图分享下载上搜索。
1、4.5 一阶谓词语义系统4.5.1 什么是形式系统语义抽象公理系统或者形式系统，具有较高的抽象性。因此，已经脱离了任何一个具体的系统，但是我们可以对形式系统作出各种解释。通过这种解释将形式系统对应到各种具体的系统中取。例如可以将一阶谓词逻辑系统，解释到平面几何系统中。怎样将形式系统解释成具体系统呢？我们先看下面的例子：如果我们要知道的具体的真值=1，我们至少要知道以下事情：1、 x在什么范围之内，x范围是实数。2、 f是什么？ (X+1)3、 P是什么？P代表的是大于04、 a=？a=15、 x=?，x5，4例如，我们可以作出以下解释：1、解释1：l x在实数中取值l P表示等于0l 表示x-
2、al a=5因此，公式解释为。令x=5, 则s(x) -5s(f(a,x) -I(f)(I(a),s(x)令x=6，则2、解释2：l x在实数中取值l P表示大于等于0l 表示因此，公式解释为。这个公式不必对a和x作出具体解释，就可以确定公式的真值。即对于任何实数x，和赋值映射v，。由上面的例子可以看出，要对形式系统作出解释，我们要了解以下问题： x取值于哪里？即规定讨论问题的领域。 给出谓词的含义和谓词的真值 给出函数的解释 给出变量和常量的值 根据连接词的赋值规则，赋值这就是我们要研究的语义系统指称语义的主要内容。现代逻辑语义学理论的创始人是美籍波兰逻辑学家、哲学家A. Tarski，其奠
3、基性文章是他在1933年发表的形式语言中的真实概念。后来被称为模型论标准语义学理论。进一步的发展由维特根斯坦最早提出设想，卡尔纳普最早把它展开为系统。这体现在他1947年发表的 意义和必然性一书中；卡普兰克里普克(S.kripke)和蒙太古作出了进一步的贡献，提出了非经典逻辑的语义学理论模态逻辑语义学(克里普克结构)。4.5.2 形式语义基本概念1、 指称语义：语义是由语义结构和以及在这种结构下公式赋真值的规定构成的。2、 语义结构：对于抽象公理系统或形式系统作出的一种解释。包括个体域和在这种个体域上的个体运算和个体间关系。下面给出形式系统语义的定义：3、 形式语义：设FS是已经存在的形式系统
4、，FS的语义有语义结构和赋值两个部分组成：a) 语义结构：当FS的项集TERM不为空时，由非空集合U和规则组I所组成二元组（U，I），称为形式系统FS的语义结构。其中U和I的性质如下：i. U为非空集合，称为论域或者个体域；ii. 规则组I，称为解释，根据规则组的规定对项集TERM中的成员指称到U中的个体；规定对原子公式如何指称到U中的个体性质（U的子集）、关系（的子集）。b) 指派：若形式系统FS中的变量集合Variables非空，那么下列映射称为指派：s：variblesU。对于给定的语义结构，可以将指派扩展到项集TERM上：TERMU； S(t) 当t 为变元 S指派t中变元由解释确定
5、当t为非变元 F(x,a) = I(f) (x, I(a) = s1( I(f) (x, I(a) = I(f) (s(x), I(a)P(f(a,x) =I(P)(I(f)(a,s(x)c) 赋值：是指一组给公式赋值的规则，据此规则可对每一结构U和指派S确定一由原子公式到值域的映射v：atomicvalue。根据这个赋值规则，可以将赋值映射进行扩展：v为：d) 可满足：公式A称为可满足，如果存在结构S与指派s，使一个赋值映射v满足v(A)=1,否则为不可满足。|=P(f(x,y)F(x,y) s(x,y)=(1,2) s(f(x,y)=I(f)(1,2)=I(f)(s(x),s(y)V(P(
6、x,y)=V(I(P)(s(x),s(y)V(I(Q)(s(x)4.5.3 一阶谓词语义1、语义结构：一阶谓词形式系统采用TARSKI语义结构。这种语义结构以为其真值集合。每一个Tarski语义结构S，由非空集合U和下列解释I构成：i 常元：对于任一常元a, I(a)U, I(a)记为，为论域中的一个元素；ii 函数： 对于任一n元函数为U的一个n元函数，记为：；iii 谓词：对于任一n元谓词，为U上的一个n元关系，记为，。当n=1时，为U的子集。2、指派：指派S为变元集合到上的映射。S可以扩展为：F(a,x)S(x)=5S(f(a,x)=I(f)(I(a),S(x)= I(f)(I(a),5
7、)i 对于每一变元v：；ii 对于每一常元a：；iii 对于每一个n元函词fn和项t1，t2.tn：S(F(x1,x2)=F(S(x1),S(x2)由此可见，指派与结构无关，而与结构相关。3、赋值：i 赋值映射v：Atomic定义为：对任何n元谓词及项t1tn，当且仅当，其中。Y=X+1P(x,y), I(P)=, , s(x)=3, s(y)=2?; I(P)(s(x),s(y):P()=1ii 赋值映射v按下列规则扩展，：l 对原子公式A：；l 对于公式，当且仅当；l 对于公式，当且仅当或；l 对公式，当且仅当对于U中每一元素d， ，其中表示指派S对x指派元素d。4、所有公理为永真式：我们
8、从公理中取公理5来证明，即证明|=为永真式。已知：=1求证：=1任意取一个结构，和这个结构任意一个指派，对于任意一个赋值f，满足f()=1，则f()=1.任意取一个结构,一个赋值映射f，f满足f()=1：证明：f()=1.f()=1, f()=1,证明:f()=1D, B(d)=1;f(AB)(d)=1 f(A(d)B(d)=1; f(A)(d)=1f(A(d)=0,或者f(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 f( (A(Sx|d)B(Sx|d) =1 A(d)=1,A(d)B(d)
9、对于论域中的任意一个个体，d, f(A(Sx|d)1求证：对于论域中的任意一个个体，d, f(B(Sx,|d)1证明：只要证明对任意结构U和指派S，对于任一赋值v：成立。由演绎定理可知，要证明，则只需证明：。因此，只需证明对于任意结构U和指派S，如果U和S满足：和成立；则在结构U和指派S下在S和U下成立。只需对任意元素d，进行验证：对于和任意赋值v由于：（1）已知（2）已知由（1）可知，或者或者。由（2）可知，因此。因此，命题成立。5、语义构造的例子一阶谓词形式系统的语义结构为：只有一个函词、一个谓词和一个常元的形式系统（推理和符号与一阶谓词相同）。P2, f1,a个体域：，即自然数集合N谓词
10、：为N上的关系。函词：为N上的后继，即常元：判断以下公式的真值：=1 v1v2P(v1+1,v2)=1P(x1+1, x1+2)=04.6 一阶元理论4.6.1 语法构成对于一阶谓词形式系统的语法构成，主要有以下定理： 独立性：FSFC的公理集合是独立的。 一致性：FSFC是一致的，即不存在FSFC的公式A，使A及同时成立 FSFC是不完全的，即存在FSFC的公式A，使A及都不成立。只需证明对于原子公式P(x), P(x), 均不成立。* FSFC的不一致扩充为完全的。A4 -(A-(B-A) 半可判定性：FSFC是半可判定的，即存在一个机械的实现过程，能对FSFC中的定理作出肯定判断，但对非
11、定理的FSFC公式未必能作出否定判决。推广：设为FSFC的一个可判定公式集（递归集），那么的演绎结果集合是半可判定的。4.6.2 语义结构对于一阶谓词形式系统的语义主要有以下定理： 紧致性：对FSFC的任何公式集合，如果的所有有穷子集可满足，那么也是可满足的。证明：同命题逻辑。反证法4.6.3 语法语义关系语法语义关系，主要有以下定理： 合理性：对于FSFC中任一公式A，如果A，那么|=A。合理性推广：对于FSFC的任一公式集和公式A，若A,则|=A。证明简单，与命题逻辑基本相同。合理性推论：对于FSFC中任意公式A,B，若AB，则A|=B 完备性：对于FSFC的任一公式A，如果|=A，那么A
12、。Godel完备性定理：对于FSFC的任一公式集和公式A，如果|=A，则A。已知：对于任意的结构，和任意的赋值映射f,如果f使得f()=1，则f(A)=1.求证：存在一个证明序列A1,An=A，其中Ai或者为公理，或者为中的元素，或者是由前边的通过推理规则得到。证明：对于FSFC的任一公式集是一致的，充要条件为是可满足的。完备性定理又被称为Godel完备性定理，其证明思路如下：（1） 对于一阶谓词任意公式集合是一致的，则存在一个一致公式集合，满足如果公式集合K包含，且K是一致的，则。成为的最大一致扩充。A1,A2,A3=A1,A2,A3,A4=f(A1,A2,A3)=1;f(A)=1;f1(A
13、1,A2,A3,A4,A)=1;F1(A)=1（2）对于的最大一致扩充和公式A，如果A，则有。（3）反证法：假设A ，故有A，从而为一致的。由（1）可知，存在着一极大一致集F，使得AF(或者AF)。根据前提|=A ，F|=A。由（2）可知F。这与F的一致性矛盾。 5 归结原理及应用5.1 标准形式公式标准化的主要目的是对公式进行机械化推理过程。机械化推理过程，是知识工程、逻辑程序设计、人工智能和定理机器证明等理论的基础。在讲述公式标准化过程之前，我们首先介绍整个形式逻辑的基本发展思路。推理过程： 语义 逻辑推理 反证，真值表合理、完备 公式形式系统 公理，规则（分离规则）（机器难以识别）同可满
14、足 标准形式标准形式 ，代替（机械化）B:B A,A =0假设公式集合S=A1,A2,.,An,假设T=B1,B2,B3,.,Bm这是标准型，这个标准型T和S之间是同可满足的。如果S是可满足的，则T是可满足的。如果T是不可满足的，则S是不可满足的。, x=3, B RETE=NETWORK 1965 HPROLOG , 1982 :RULE ENGINE-ILOG目标：反向推理B, B 0:一个集合F化简到标准型S，如果集合F是可满足的，则标准型S是可满足的。S上出现了0。S是不可满足。如果S是不可满足的，则F是不可满足计算语言Descriptive programming , functio
15、nal programming language =Rule engine forward PROLOG , LISP 5.1.1 前束范式1、前束范式：称FSFC的公式为前束范式，当且仅当它有下面的形式：其中Qi,I=1.n是量词。并且B不含量词，称Q1Qn为前束词，称B为母式；2、求前束范式a) ；b) ，当x在A中不自由出现；，当x在A中不自由出现；如果有自由出现时，采用改名原理。c) ；=1,2,10A(1)=A(10)=1或者B(1)=B(10)=1 A(1)vB(1)A(1)vb(1)=A(10)VB(10)=1,或者A(1),A(10)=0或者B(1),B(10)=1A1,3,5
16、,7,9=1, B(2,4,6,8,10)=1A(2,4,6,8,10)=0, B(1,3,5,7,9)=0|=|； 1,2,3 A(1)=1;A(2)=0,A(3)=0A(1)=1, B(1)=0;A(2)=0, B(2)=1;A(3)=0=B(3)=0 B(2)=0,B(1)=0,B(3)=0X=1, A(1)&B(1)=0,x=2, A(2)&B(2)=0, x=3, A(3)&B(3)=0xA(x)&vxB(x)d) ，当x不在B(y)中出现，且y不在A(x)中出现;，当x不在B(y)中出现，且y不在A(x)中出现;如果有自由出现时，采用改名原理。4、 例：将化成与其等价的前束范式。(
17、 (x$yF(u,x,y) ($x(yG(y,w)H(x) (x$yF(u,x,y) ($x(yG(y,w)H(x) (x$yF(u,x,y) ($xy(G(y,w)H(x) ($x$yF(u,x,y)$xy(G(y,w)H(x)($xyF(u,x,y)$xy(G(y,w)H(x)$x(yF(u,x,y)y(G(y,w)H(x)$x(yF(u,x,y)y(G(y,w)H(x)x(yF(u,x,y)y(G(y,w)H(x)x (yF(u,x,y) y(G(y,w)H(x)x ($yF(u,x,y) $y (G(y,w)H(x)x ($yF(u,x,y) $y ( G(y,w) H(x)x ($y
18、F(u,x,y) $z ( G(z,w) H(x)x $y$z (F(u,x,y) G(z,w) H(x)2、定理：对于FSFC中的任一公式，有一个前束范式与其逻辑等价。证.证明实际上是一转换算法：.联结词归约：消去，；.否定词深入：将否定词移到到每个原子公式之前;.约束变项改名：将每个约束变项都改名为互不同名，且与所有的自由变项也不同名;.量词与$前移：将所有的量词按其在公式中的位置顺序全部移到整个公式之前;.调整与：将母式化归为CNF。证明完毕。5.1.2 斯柯伦标准形1 标准化前束范式：基础，但不够用。例如： A(a)匹配规则比较麻烦，而且是机器难于识别的。 B(a) 匹配规则比较麻烦，
19、而且是机器难于识别的。那么怎样让计算机能够匹配这些公式的关键在于怎样去掉量词；对于可以去掉（可满足性），而则不成。因为：l 与A(c)并不逻辑等价；由；不可能得到，A(c)成立。l (x,f(x) 就更难了；对A(x,c)，要对每一x找到不同的常量c才行。(1,2), (2,f(x),.利用计算机进行逻辑推理的时候，并不需要对公式进行等价转换。只需要和销去量词后的公式保持同可满足性即可。斯柯伦标准型就是为了解决以上的问题。1,2,102、Skolem定理在介绍Skolem定理之前，我们首先看看反证法：证明成立，只需证明为不可满足的。设与公式集合1. n同可满足。要证明为不可满足的，则只需证明I
20、为不可满足的，其中I为1到n中任意的数字。I的不可满足性，就证明了。从而在将公式化为标准形式，不需要之间是等价的，只需时同可满足的。Q1Q2Q30如果存在一个赋值映射f，使得f()=1,则存在一个赋值映射f1，使得f1(Q1)=1.S1与S2是同可满足的：指的是如果存在赋值f(S1)=1，则存在赋值f1(S2)=1.A1,A100, A2,A1Skolem定理：对于公式，存在一个不在A中出现的常元c，使得与公式具有同可满足性；对于公式存在一个不在A中出现的函数，使得公式与公式具有同可满足性。其中c称为斯柯伦常元、称为Skolem函词。3、skolem标准形设公式A为前束范式（其母式为析取范式和
21、合取范式）。称为A的斯柯伦标准形，如果是用skolem常元、skolem函词消除A中量词后得到的公式。当A的母式为合取范式时，其斯柯伦标准形称为合取型，否则称为析取型。斯柯伦标准型通常的约定为合取型。例：求公式的斯柯伦标准型。求一个公式a的Skolem标准型的算法： .先将a化为前束范式b1:=Qx1QxnA，其中A为母式，不含量词。若所有的Qi:=(1 i n)，则b1显然是Skoloem标准型。取b:=b1 ，即为所求。算法结束;否则转2 ：2.若b1形为$x1 x2xn A，则选一不在A中出现的个体常项c(称为Skolem常项),可得 b2:=x2xn 显然b2是一Skolem标准型。取
22、b :=b2 ，即为所求。算法结束; .若b1形为x1xk$xk+1Qk+2xk+2QnxnA，则选一不在A中出现的k元函词符号f(称为Skoloem函词)，可得 b2:=x1xkQk+2xk+2Qnxn若Qk+2 , Qn全为，则显然b2是一Skolem标准型。取b :=b2 ，即为所求。算法结束; 否则返回到自己。完毕。A1=(B1vb2)()()=B1vB2, (), () A, AvB, BA2=B1B2B3B4 =B1,B2,B3,BA1,A2,A3 =A1A2A3 5.1.3 子句集A1,A2,A3= A1&A2&A31、子句集概念对于合取型斯柯伦标准型，其合取项被称为子句，其析取
23、项被称为文字。由于每个合取型斯柯伦标准型，有多个子句构成。我们可以把一个斯柯伦标准型中的所有子句集合在一起。这样一个斯柯伦标准型，就有了一个与其对应的等价的子句的集合。公式Skolem AC1&C2&C3=C1,C2,C3:C1=L1vL2vL3.公式集合S被称为公式A的子句集，如果S为A的斯柯伦标准型中全体子句的集合。S称为可满足的，如果存在一个结构使S中的每个子句为真；否则称子句集合为不可满足的。公式前束范式Skolem标准型子句集例如：子句 文字 (P(x1)vP2(x2), P3(x2)A1A2A3=A1,A2,A32、子句集性质l 子句集中两个子句中变量是独立的、无关的，不管子句中的
24、变量名称是否相同。这主要是因为：。同一子句中的变量是相互依赖的。l 斯柯伦标准型与源公式之间是同可满足的，斯柯伦标准型与子句集之间是等价的。因此，子句集与原公式之间是同可满足的。l 如果子句集是可满足的，则子句集的子集都是可满足的。相反，如果一个子句集的子集是不可满足的，则子句集是不可满足的。A1,A2,A10:可满足：f(A1)=f(A2)=f(A10)=1, 任意子集都是可满足的。A1,A2,A10：不可满足的：f(A1)=f(A2)=f(A9)=1,f(A10)=0;任一子集是否是可满足的？A1,A2,A10，A11，3、求子句集通常通过以下步骤，可以得到一个公式的子句集。i 求A的合取
25、型前束范式ii 求A的skolem标准形iii 将skolem标准形改为子句通过这样的过程，我们将一个公式进行了标准化的表示过程。从而使计算机的自动推理有了理论上的基础。这个过程表示如下：AB公式 前束范式 skolem标准形 子句集=同可满足等价公式合取型范式子句集A, BvC, A(x)vB, A例：求公式的子句集。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)$x(yF(u,x,y)y(G(y,w)H(x) 前束范式 合取范式 skolem标准型 子句集子句1子句2练习：1、证明：|=