《高级数理逻辑第5讲.doc》由会员分享，可在线阅读，更多相关《高级数理逻辑第5讲.doc（15页珍藏版）》请在金锄头文库上搜索。
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 标准形式公式标准化的主要目的是对公式进行机械化推理过程。机械化推理过程，是知识工程、逻辑程序设计、人工智能和定理机器证明等理论的基础。在讲述公式标准化过程之前，我们首先介绍整个形式逻辑的基本发展思路。推理过程： 语义 逻辑推理 反证，真值表合理、完备 公式形式系统 公理，规则（分离规则）（机器难以识别）同可满足 标准形式标准形式 ，代替（机械化）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是可满
