高级数理逻辑第11讲全解

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

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

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

4、AIXIOM 为公理集； RULE 为推理规则集。 ：1、符号表为非空集合，其元素称为符号。2、设 * 为上全体字的组合构成的集合。 项集 TERM 为 * 的子集， 其元素称为项； 项集 TERM 有子集 VARIABLE 称为变量集合，其元素称为变量。3、设 * 为上全体字的组合构成的集合。公式结FORMULA 为 * 的子集，其元素称为公式；公式集有子集 ATOM ，其元素称为原子公式。4、公理集 AXIOM 是公式集 FROMULA 的子集，其元素称为公理。5、推 理 规 则 集 RULE 是 公 式 集 FORMULA 上 的 n 元 关 系 集 合 ， 即nRULE= r | n（

5、n是正整数 n 2 r FORMULA n） ，其元素称为形式系统的 推理规则。其中公式集和项集之间没有交叉， 即 TERM FORMULA = ，公式和项统称为表达式。由定义可知，符号表、项集TERM 、公式集 FORMULA 是形式系统的语言部分。而 公理集 AXIOM 、推理规则集 RULE 为推理部分。形式系统的重要问题1、符号表 为非空、可数集合（有穷、无穷都可以） 。2、项集 TERM 、公式集 FORMULA 、公理集 AXIOM 和推理规则集 RULE 是递归集合， 即必须存在一个算法能够判定给定符号串是否属于集合。3、形式系统中的项是用来描述研究的对象，或者称为客观世界的。而

6、公式是用来描述 这些研究对象的性质的。这个语言被称为对象语言。定义公式和项产生方法的规则 称为词法。4、用来描述形式系统中各个部分性质的语言称为元语言。用于研究形式系统的元语言又被称为元数学。形式推导1、基本概念演绎结果与定理 ：设 A为FSPC上一公式， 集合 为 FSPC上一公式集合。 称A 为 的 演绎结果，记为 A ，如果存在一个公式序列：A1,A2,A3, ,AL( A) 使得 Ai 或者为形式系统 FSPC 的公理，或者为公式集合 中的元素，或者或者为Aj1,Aj2,Aj3, ,Ajn 1（j1,j2, j3, , jn 1 i ）由推理规则 r得到；则称 A 为 FSPC的演 绎

7、结果。当 时，称 A 为定理 FSPC上的定理。称 A1,A2,A3, ,AL（ A）为 A 的 证明序列。逻辑等价： 公式 A 和 B 分别为两个公式，如果 A,B 满足 B A，且 AB 同时成立，则 称公式 A和 B为逻辑等价公式，记为 A B。即 A,B互为演绎结果。例如： A| A， A B| B A， A B | B A。对偶：设 A 为 FSPC 上由联结词 , , 和原子公式构成的公式。 在 A 中交换 和 ， 以及原子公式和他的否定公式，得到公式A' ，则称 A' 为 A 的对偶。2、推理基础（1）公理代入原理：设 A（P）为含有变元 P 的公理（定理同样适用

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

9、得到公式 A '，则 A '为 A 的改名式；如果 A '是 A 的改名式，且 A '改用的变元在 A 中无任何出现，那 A A'3、其他推理方法 根据形式系统的性质，给出一些专用推理规则。语义系统语义系统定义形式语义：设 FS 是已经存在的形式系统， FS的语义有语义结构和赋值两个部分组成：a）语义结构： 当 FS 的项集 TERM 不为空时，由非空集合 U 和规则组 I 所组成二 元组（ U，I），称为形式系统 FS的语义结构。其中 U和 I的性质如下：i. U 为非空集合，称为论域或者个体域；ii. 规则组 I，称为解释，根据规则组的规定对项集TE

10、RM 中的成员指称到 U中的个体；规定对原子公式如何指称到 U 中的个体性质（ U 的子集）、关 系（ U n 的子集）。b）指派： 若形式系统 FS中的变量集合 Variables 非空，那么下列映射称为指派： s： varibles >U。对于给定的语义结构，可以将指派扩展到项集TERM 上：s ：TERM >U ；s S（t）当 t 为变元S 指派 t 中变元由解释确定当 t 为非变元c）赋值：是指一组给公式赋值的规则， 据此规则可对每一结构 U 和指派 S 确定一 由原子公式到值域的映射 v：atomic >value。根据这个赋值规则， 可以将赋值 映射进行扩展：

11、v 为 v ：Formula >value 。元理论语法构成（1）独立性： 如果形式系统中每一个公理都是独立的，即把任一公里A 从形式系统中删除后，所得形式系统 FS不满足 FSA（即 A 不是 FS的定理），则称形式系统为独 立的；独立形式系统是简洁的；（ 2）一致性： 形式系统 FS称为一致性，或相容的（ consistent ）如果不存在 FS的公 式 A，使得 A， A 同时成立；所有形式系统都应该是一致的；（ 3）完全性： 形式系统为完全的，如果对形式系统中任意公式A，或者 A 成立，或者 A 成立；完全性的形式系统，一切都是可知的；因此，几乎没有价值；FS 对的任一公式4）可

12、判定性： 形式系统 FS 称为可判定的，如果存在一个算法，对A ，可确定 A是否成立， 否则称 FS 是不可判定的； 如果上述算法对定理能作出判 断，而对于非定理未必终止（作判断） ，称 FS 为半可判定的；FS 为可判定的，当且仅当定理集合为递归集；( 5)公式集合一致性： 称形式系统的公式集合 为一致的，如果形式系统是一致的， 且不存在公式 A 使 A ， A 同时成立。语义系统基本上没有。语法语义关系研究语法语义关系， 首先关心的问题是在语法上的形式演算， 在语义的逻辑推论上是否 成立。这个问题被称作合理性( Soundness)。其次，是对于语义上的逻辑推理，在形式 演算上是否成立。这

13、个问题是完备性(Completeness)。这两个问题是语法语义关系的核心。1) 合理性( soundness)：称形式系统 FS是合理的， FS的任意公式 A 有：FS A， 则 M A ， M为所有结构；2) 完备性( Completeness)：称形式系统 FS 是完备的，如果对 FS 的任意公式 A 有：若 M A，则 FS A ，这里 M为 FS所讨论的一类结构；3) 紧致性：称形式系 FS是紧致的， 如果对 FS的任意公式集 有：如果公式集 的所有穷子集是可满足的，那么公式集 也是可满足的；归结原理归结方法二元归结： 设 C1 和 C2 分别含有文字 L1和 L2 的子句，并且 L

14、1 和 L2 有最一般合一 ， 那么下列推理规则称为归结原理：C1,C2(C1L1 ) (C2 L2 )归结过程公式集 前束范式 skolem 标准形 子句集 合一 归结 合一与代换：子句集合一后与原子句集之间的逻辑关系； 合一是代换( t1/x1 tn/x n)将子句集中的变量 xi 代换为项 ti; 归结合理与完备：在合一后的子句集上归结是一种推理，那么推理能否保证合 理性与完备性；提高效率的策略： 删除策略；支持集策略；线性策略；在归结过程中， 注意： 代换过程如果出现 P(a), P(b) 的情况就很可能是代换出现的问题；元定理在归结原理中，我们给定的形式系统是： 形式系统是子句集，其

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

16、些正规系统中，最简单的是 NSK 系统。下面 我们给出 NSK 系统的构成。1、 NSK 系统语言部分符号表： p1 , p2 , , , ,(,) ；其中 pi 为原子命题， , 为联接词， , 为模态词， (,) 技术符号。项集：空集。 公式集：由以下递归定义：1) pi为公式 (i=1,2,3,4 )2) 如A,B 为公式,那么( A B),( A),( A),( A )都是公式3) 除由 1,2 得到外 , 无其它公式2、NSK推理部分 公理集：包含以下公理：A1 : A AA2 :(AB)( A B) ；通常被成为 K公理A3 : 全部重言式A4 : A （ 当 A为公理）推理规则：

17、分离规则 A B, A, B其他概念与 FSPC 的概念相同，如定理、证明序列等。语义结构1、正规结构定义我们知道， 对于每个命题的真假都是和可能世界之间有着密切的关系。 对于正规系统的 语义，必须考虑可能世界。可能世界是非常多的，可能世界构成一个集合。每个可能世界对应于不同的场合， 可能世界之间是可变换的。 能够从一个可能变换到另 一个可能世界。从一个可能世界，能否变换到另一个可能世界在赋予真值时是非常重要的。 例如，如果一个可能世界不能变换到其他的可能世界上，那么在这个可能世界所讨论的 A 和A 真都是指 A真这一个概念（当然，我们假设这种关系具有自反性的条件下）。可能世界之间的这种关系，

18、实际上是可能世界的集合中的元素之间的关系。有了这种可能世界的集合和可能世界之间的关系， 那么我们就可以对正规系统中任何公 式赋予一定的真值。正规结构： 有以上分析可知，对于正规系统语义被成为正规结构，正规结构是指三元组 <U,R,I> ， 其中：U 为一非空集合，称为宇宙；其成员为可能世界，可能世界用wi 来标记；R为 U 上的一个二元关系，称为可能世界间的可达关系；I 为赋值映射，是U P1P .到 0,1 上的映射； 即对在每一个可能世界中，对原子命题 Pi 赋值；2、 正规结构的一些解释 我们对正规系统中的一些公式进行解释，从而能够更加了解可能世界的概念。 kw A 表示：指在宇宙中 k 的 w 可能世界中， A 为假 kw A 表示：对于所有 w' U ， w'Rw， kw 'A ，即 A 为真；kw A表示：存在 w' U ，且 w