北邮高级数理逻辑课件.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), AB4、 公理集AXIOM是公式集FROMULA的子集，其元素称为公理。5、 推理规则集RULE是公式集FORMULA上的n元关系集合，即RULE=，其元素称为形式系统的推理规则。其中公式集和项集之间没有交叉，即TERMFORMULA =，公式和项统称为表达式。由定义可知，符号表、项集TERM、公式集FORMULA是形式系统的语言部分。而公理集AXIOM、推理规则集RULE为推理部分形式系统特性1、 符号表为非空、可数集合（有穷、无穷都可以）。2、 项集TERM、公式集FORMULA、公理集AXIOM和推理规则集RULE是递归集合，即必须存在一个算法能够判定给定符号串是否属于集合（可判定的）。3、 形式系统中的项是用来描述研究的对象，或者称为客观世界的。而公式是用来描述这些研究对象的性质的。这个语言被称为对象语言。定义公式和项产生方法的规则称为词法。公理：IIIIII证明：AA(1)A(AA)(A(BC)(AB)(AC)(A(BA)(AB)(AA)(A(AA)A)(A(AA)(AA)A(AA)A)(A(AA)(AA)(A(AA)AA分离规则已知：R是一个有关公式的性质证明：R对于所有公式有效I. 对于，则II. 假设公式A和B都具有RIII. ，且，则IV. 是公式，如果且，则根据：形式系统的联结词只有两个，因为在命题逻辑的语义上，其他联结词可以有这两个联结词表示。已知：求证：A成立(1)A是公式(2)，反证(3) 3公理代入原理：设A(P)为含有变元P的公理（定理同样适用），如果将公式A中的变元P替换为命题变元B，则A(B)仍为公理（定理）；（公理填充）等价替换原理：设命题公式A含有子公式C（C为命题公式），如果CD，那么将A中子公式C提换为命题公式D（不一定全部），所得公式B满足AB。紧致性：设为FSPC上的公式集合，A为FSPC的公式。如果，则存在的有限子集0 使得0 。已知：A(BC), B证明：AC公理推演：A(BC)ABC BC自然推演：f(B)=1,f(A)=0或者f(BC)=1。假设f(A)=0;则f(AC)=1.假设f(A)=1,那么f(BC)=1.f(B)=1,则f(C)=1.因此，f(AC)=1.由此，命题成立。给出一个形式系统，其公理定义如下：A, (,), ,-给出公理如下：AAAAA(AA)(AA)(AA)(AA)(A-A-A)-(A-A)下列哪些是定理？AA(AA)(AA)(AA)(AA)(AAA)(AAA)(AB)(AB)(AB)语义构成结构：（有两个主要部分构成）*确定研究对象集合，论域或个体域*把形式系统中的变量到论域中的一组规则映射规则域值：指一组给公式赋值的规则根据这项规则将 AtomicValue中语义的特殊公式1) 公式A为永真式，重言式tautologies，如果对一切赋值，.2) 公式A为永假式，矛盾式contradictions,如果对一切赋值，3) A，B为逻辑等价的，如果对于一切赋值，记做AB(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(AB)=1;由于f1(AB)=1,并且f1(A)=1，则f(B)=1充分性：对于映射f，若f()=1，假设f1(A)=0;f1(AB)=1.假设f1(A)=1, 由于已知条件可以知道f(B)=1.因此，f(AB)=1从形式上：必要性：1成立，则成立。对于成立有两种情况，为了证明成立，只需考虑，使1的情况。如果赋值映射v，满足1，1且，则有1。因此，成立。充分性：任取赋值映射v，满足，则有：当0时，有当1时，由已知1， 因此联结词的完备集：联结词的集合为完备的，当且仅当对于其他的联结词都可以由这个联结词的集合中的元素来表示。FSPC中的完备集：、等。如果引入异或，那么异或与也构成一个完备集合。形式化系统语义结构元理论自动化语法构成语法构成研究形式系统语言构成规律。主要研究推演（重写）规律；主要规律：（1）独立性：如果形式系统中每一个公理都是独立的，即把任一公里A从形式系统中删除后，所得形式系统FS不满足FSA（即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。假设：nU。对于给定的语义结构，可以将指派扩展到项集TERM上：TERMU； S(t) 当t 为变元 S指派t中变元由解释确定 当t为非变元c) 赋值：是指一组给公式赋值的规则，据此规则可对每一结构U和指派S确定一由原子公式到值域的映射v：atomicvalue。根据这个赋值规则，可以将赋值映射进行扩展：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元谓词及项t1tn，当且仅当，其中。ii 赋值映射v按下列规则扩展，：对原子公式A：；对于公式，当且仅当；对于公式，当且仅当或；对公式，当且仅当对于U中每一元素d， ，其中表示指派S对x指派元素d。已知：任意取一个结构,一个赋值映射f，f满足f()=1：证明：f()=1.设x取值为df(AB)(d)=1 f(A(d)B(d)=1; f(A)(d)=1f(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:=Qx1QxnA，其中A为母式，不含量词。若所有的Qi:=(1 i n)，则b1显然是Skoloem标准型。取b:=b1 ，即为所求。算法结束;否则转2 ：2.若b1形为$x1 x2xn A，则选一不在A中出现的个体常项c(称为Skolem常项),可得 b2:=x2xn 显然b2是一Skolem标准型。取b :=b2 ，即为所求。算法结束; .若b1形为x1xk$xk+1Qk+2xk+2QnxnA，则选一不在A中出现的k元函词符号f(称为Skoloem函词)，可得 b2:=x1xkQk+2xk+2Qnxn若Qk+2 , Qn全为，则显然b2是一Skolem标准型。取b :=b2 ，即为所求。算法结束; 否则返回到自己。子句集概念对于合取型斯柯伦标准型，其合取项被称为子句，其析取项被称为文字。由于每个合取型斯柯伦标准型，有多个子句构成。我们可以把一个斯柯伦标准型中的所有子句集合在一起。这样一个斯柯伦标准型，就有了一个与其对应的等价的子句的集合。公式Skolem AC1&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)vL1C2=(C2-L2)VL2f(C1)=1，f(C2)=1 f(L1)=1,则f(L2)=0f(L1)=0,则f(L2)=1f(c)=f(C1-L1)v f(C2-L2)C1=(c1-l1)vL1f(l1)=0, f(c1-l1)=1 因此，f(c)=1f(l1)=1，f(l2)=0，则f(c2-l2)=1，f(c2)=f(c2-l2)Vf(l2)f(c)=1代换需要注意的是：首先代换不能是自身代换，用同一变量代换本身是没有什么意义的；其次，对于代换的过程是一次性将所有的变量同时代换成项，而不是先代换第一项，再代换第二项的顺序结构。设公式为，代换为，求代换结果。：f(y)/xOz/y，同时代换结果：P(f(y),z,z)f(y)/x*z/y，先进性前一项代换，再进行后一项代换,=结果：P(f(z),z,z)合一既然有了代换的概念，我们必然要考虑，能够将一些不同公式通过代换化为