高级数理逻辑第11讲

1、总复习本章对高级数理逻辑所讲述的内容总结，并对已经学习的内容进行回顾。在对所讲述的内容回顾之前，首先对整个数理逻辑学科的组成进行回顾，从而使大家有更深刻的认识。数理逻辑学科学科发展从数理逻辑学中衍生出来的学科有很多，如：递归论、可计算理论、模型论、机器证明、知识工程、布尔代数等。这些理论都是以数理逻辑学为基础的。针对数理逻辑本身，由于这些学科的需求产生了很多不同种类的逻辑系统。数理逻辑的不同种类，基本上都是从经典的逻辑系统中扩展而来的。这种扩展通常有语法扩展和语义扩展。l 语法扩展：在经典逻辑系统中，扩充一些符号，从而衍生出新的逻辑系统。如模态逻辑，二阶谓词逻辑等。l 语义扩展：对逻辑系统中语

2、义的范围等进行扩展，如模糊逻辑等。数理逻辑通常划分成以下不同种类的逻辑系统：1、 经典逻辑：传统的命题逻辑、一阶谓词逻辑等。认为世界是黑白的，对于一个命题非真既假。2、 模态逻辑：认为世界上任何事情的真假是与时间有着密切的关系的。3、 多值逻辑：认为世界上的对与错是没有绝对的，命题的真假是可以是多个甚至连续值的。4、 非单调逻辑：讨论如何将人类的常识加入到逻辑系统中去。经典逻辑是单调逻辑，既事实越多，已有的结论不会消失；而单调逻辑中，可能随着事实的增加原有的结论被否定。体系构成在高级数理逻辑（计算逻辑）中，每一种逻辑都自成体系。逻辑的体系过程主要包括以下几个方面：1、 形式系统：用符号的方式来

3、描述一个逻辑系统的构成。类似于形式语言系统。2、 语义系统：针对形式进行解释的一套体系，这套体系确定了符号的含义的解释方法和规则。3、 元理论：对形式系统组成、语义系统特性和形式与语义之间关系进行研究。从而保证了数理逻辑的初衷（利用数学演算的方法来研究人类思维过程）。4、 自动化推理：在形式系统的基础上，研究利用计算机自动进行推理的理论和方法。以及自动推理的效率提高方法和自动推理完备性研究。形式系统形式系统构成形式系统由, TERM, FORMULA, AXIOM, RULE等5个部分构成，其中 称为符号表，TERM为项集；FORUMULA为公式集；AIXIOM为公理集；RULE为推理规则集。

4、：1、 符号表为非空集合，其元素称为符号。2、 设为上全体字的组合构成的集合。项集TERM为的子集，其元素称为项；项集TERM有子集VARIABLE称为变量集合，其元素称为变量。3、 设为上全体字的组合构成的集合。公式结FORMULA为的子集，其元素称为公式；公式集有子集ATOM，其元素称为原子公式。4、 公理集AXIOM是公式集FROMULA的子集，其元素称为公理。5、 推理规则集RULE是公式集FORMULA上的n元关系集合，即RULE=，其元素称为形式系统的推理规则。其中公式集和项集之间没有交叉，即TERMFORMULA =，公式和项统称为表达式。由定义可知，符号表、项集TERM、公式集

5、FORMULA是形式系统的语言部分。而公理集AXIOM、推理规则集RULE为推理部分。形式系统的重要问题1、 符号表 为非空、可数集合（有穷、无穷都可以）。2、 项集TERM、公式集FORMULA、公理集AXIOM和推理规则集RULE是递归集合，即必须存在一个算法能够判定给定符号串是否属于集合。3、 形式系统中的项是用来描述研究的对象，或者称为客观世界的。而公式是用来描述这些研究对象的性质的。这个语言被称为对象语言。定义公式和项产生方法的规则称为词法。4、 用来描述形式系统中各个部分性质的语言称为元语言。用于研究形式系统的元语言又被称为元数学。形式推导1、 基本概念演绎结果与定理：设A为FSP

6、C上一公式，集合为FSPC上一公式集合。称A为的演绎结果，记为，如果存在一个公式序列：使得或者为形式系统FSPC的公理，或者为公式集合中的元素，或者或者为由推理规则r得到；则称A为FSPC的演绎结果。当时，称A为定理FSPC上的定理。称为A的证明序列。逻辑等价：公式A和B分别为两个公式，如果A,B满足B，且AB同时成立，则称公式A和B为逻辑等价公式，记为AB。即A,B互为演绎结果。例如：|，|，|。对偶：设A为FSPC上由联结词, , 和原子公式构成的公式。在A中交换和，以及原子公式和他的否定公式，得到公式，则称为A的对偶。2、 推理基础（1）公理代入原理：设A(P)为含有变元P的公理（定理同

7、样适用），如果将公式A中的变元P替换为命题变元B，则A(B)仍为公理（定理）；Cà(BàC)àC)（2）等价替换原理：设命题公式A含有子公式C（C为命题公式），如果CD，那么将A中子公式C提换为命题公式D（不一定全部），所得公式B满足AB。（3）对偶原理：设A为FSPC上的公式，为其对偶，则A。（4）演绎定理：设为任一公式集合, A,B为任意公式,那么：，AB 当且仅当，AB 当且仅当（5）(变量)改名原理如果公式A中至少一个量词的指导变元和相应的约束变元都改名为另一个相同变元后得到公式A，则A为A的改名式；如果A是A的改名式，且A改用的变元在A中无任何出现，那A

8、A3、 其他推理方法根据形式系统的性质，给出一些专用推理规则。语义系统语义系统定义形式语义：设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&

9、gt;U。对于给定的语义结构，可以将指派扩展到项集TERM上：TERM>U； S(t) 当t 为变元 S指派t中变元由解释确定 当t为非变元c) 赋值：是指一组给公式赋值的规则，据此规则可对每一结构U和指派S确定一由原子公式到值域的映射v：atomic>value。根据这个赋值规则，可以将赋值映射进行扩展：v为：Formula>value。元理论语法构成（1）独立性：如果形式系统中每一个公理都是独立的，即把任一公里A从形式系统中删除后，所得形式系统FS不满足FSA（即A不是FS的定理），则称形式系统为独立的；l 独立形式系统是简洁的；（2）一致性：形式系统FS称为一致性，或相

10、容的（consistent）如果不存在FS的公式A，使得A，同时成立；l 所有形式系统都应该是一致的；（3）完全性：形式系统为完全的，如果对形式系统中任意公式A，或者A成立，或者成立；l 完全性的形式系统，一切都是可知的；因此，几乎没有价值；（4）可判定性：形式系统FS称为可判定的，如果存在一个算法，对FS对的任一公式A，可确定A是否成立，否则称FS是不可判定的；如果上述算法对定理能作出判断，而对于非定理未必终止（作判断），称FS为半可判定的；l FS为可判定的，当且仅当定理集合为递归集；（5）公式集合一致性：称形式系统的公式集合为一致的，如果形式系统是一致的，且不存在公式A使A ， 同时成立

11、。语义系统基本上没有。语法语义关系研究语法语义关系，首先关心的问题是在语法上的形式演算，在语义的逻辑推论上是否成立。这个问题被称作合理性（Soundness）。其次，是对于语义上的逻辑推理，在形式演算上是否成立。这个问题是完备性（Completeness）。这两个问题是语法语义关系的核心。1) 合理性（soundness）：称形式系统FS是合理的，FS的任意公式A有：FS，则M，M为所有结构；2) 完备性（Completeness）：称形式系统FS是完备的，如果对FS的任意公式有：若M，则FS，这里M为FS所讨论的一类结构；3) 紧致性：称形式系FS是紧致的，如果对FS的任意公式集有：如果公式

12、集的所有穷子集是可满足的，那么公式集也是可满足的；归结原理归结方法二元归结：设和分别含有文字和的子句，并且和有最一般合一，那么下列推理规则称为归结原理：归结过程公式集 前束范式 skolem标准形 子句集 合一 归结ü 合一与代换：子句集合一后与原子句集之间的逻辑关系；合一是代换（t1/x1tn/xn）将子句集中的变量xi代换为项ti;ü 归结合理与完备：在合一后的子句集上归结是一种推理，那么推理能否保证合理性与完备性；提高效率的策略：删除策略；支持集策略；线性策略；在归结过程中，注意：代换过程如果出现的情况就很可能是代换出现的问题；元定理在归结原理中，我们给定的形式系统是

13、：l 形式系统是子句集，其上的推理方法不在是分离规则，而是归结；l 语义系统是Herbrand结构。在这样的推理环境中，我们还是要考虑形式推理（子句集上的归结）与形式语义之间的关系。这些关系中，我们重点考虑的是合理性和完备性。1、合理性：合理性的表现有两个定理，前面已经叙述过，下面重复一下：ü 设子句集c为子句c1和c2的归结结果，则c为c1和c2的逻辑结果；ü 设子句c为子句集S的归结结果，即存在一个归结序列，得到c，则c为S的逻辑结果；2、完备性：ü 若子句集S为不可满足的，那么必定存在一个否证，即存一个导出空子句口的归结序列。模态逻辑正规系统模态逻辑是研究各

14、种不同的正规系统，这些正规系统中，最简单的是NSK系统。下面我们给出NSK系统的构成。1、 NSK系统语言部分l 符号表：,(,) ；其中为原子命题，为联接词，,为模态词，(,)技术符号。l 项集：空集。l 公式集：由以下递归定义：1) 为公式(i=1,2,3,4)2) 如A,B为公式,那么,()都是公式 3) 除由1,2得到外,无其它公式2、NSK推理部分l 公理集：包含以下公理：；通常被成为K公理全部重言式 (当A为公理)l 推理规则：分离规则 ,其他概念与FSPC的概念相同，如定理、证明序列等。语义结构1、正规结构定义我们知道，对于每个命题的真假都是和可能世界之间有着密切的关系。对于正规

15、系统的语义，必须考虑可能世界。可能世界是非常多的，可能世界构成一个集合。每个可能世界对应于不同的场合，可能世界之间是可变换的。能够从一个可能变换到另一个可能世界。从一个可能世界，能否变换到另一个可能世界在赋予真值时是非常重要的。例如，如果一个可能世界不能变换到其他的可能世界上，那么在这个可能世界所讨论的A和A真都是指A真这一个概念（当然，我们假设这种关系具有自反性的条件下）。可能世界之间的这种关系，实际上是可能世界的集合中的元素之间的关系。有了这种可能世界的集合和可能世界之间的关系，那么我们就可以对正规系统中任何公式赋予一定的真值。正规结构：有以上分析可知，对于正规系统语义被成为正规结构，正规结构是指三元组<U,R,I>，其中：l U为一非空集合，称为宇宙；其成员为可能世界，可能世界用来标记；l R为U上的一个二元关系，称为可能世界间的可达关系；l I为赋值映射，是上的映射；即对在每一个可能世界中，对原子命题Pi赋值；2、 正规结构的一些解释我们对正规系统中的一些公式进行解释，从而能够更加了解可能世界的概念。l 表示：指在宇宙中k的w可