高级数理逻辑第1讲

《高级数理逻辑第1讲》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

1、1学科介绍1.1数理逻辑介绍1.1.1什么是数理逻辑？逻辑是探索、阐述和确立有效推理原则的学科，最早由古希腊学者亚里士多德创建的。用数学的方法研究关于推理、证明等问题的学科就叫做数理逻辑。也叫做符号逻辑。数理逻辑的内容：1、命题逻辑系统2、一阶谓词逻辑系统命题演算是研究关于命题如何通过一些逻辑连接词构成更复杂的命题以及逻辑推理的方法。命题是指具有具体意义的又能判断它是真还是假的句子。如果我们把命题看作运算的对象，如同代数中的数字、字母或代数式，而把逻辑连接词看作运算符号，就象代数中的“加、减、乘、除”那样，那么由简单命题组成

2、复和命题的过程，就可以当作逻辑运算的过程，也就是命题的演算。AA->B=~AvB:BAà(BàA)这样的逻辑运算也同代数运算一样具有一定的性质，满足一定的运算规律。例如满足交换律、结合律、分配律，同时也满足逻辑上的同一律、吸收律、双否定律、狄摩根定律、三段论定律等等。利用这些定律，我们可以进行逻辑推理，可以简化复和命题，可以推证两个复合命题是不是等价，也就是它们的真值表是不是完全相同等等。命题演算的一个具体模型就是逻辑代数。逻辑代数也叫做开关代数，它的基本运算是逻辑加、逻辑乘和逻辑费，也就是命题演算中的“或”、“与”、“非”

3、，运算对象只有两个数0和1，相当于命题演算中的“真”和“假”。逻辑代数的运算特点如同电路分析中的开和关、高电位和低电位、导电和截至等现象完全一样，都只有两种不同的状态，因此，它在电路分析中得到广泛的应用。利用电子元件可以组成相当于逻辑加、逻辑成和逻辑非的门电路，就是逻辑元件。还能把简单的逻辑元件组成各种逻辑网络，这样任何复杂的逻辑关系都可以有逻辑元件经过适当的组合来实现，从而使电子元件具有逻辑判断的功能。因此，在自动控制方面有重要的应用。谓词演算也叫做命题涵项演算。在谓词演算里，把命题的内部结构分析成具有主词和谓词的逻辑形式

4、，由命题涵项、逻辑连接词和量词构成命题，然后研究这样的命题之间的逻辑推理关系。Bird(老鹰)ABird(X)A-->fly(X)BFly(鸵鸟)CP(X,y),P就是表示y>=x.y=x+1命题涵项就是指除了含有常项以外还含有变项的逻辑公式。常项是指一些确定的对象或者确定的属性和关系；变项是指一定范围内的任何一个，这个范围叫做变项的变域。命题涵项和命题演算不同，它无所谓真和假。如果以一定的对象概念代替变项，那么命题涵项就成为真的或假的命题了。命题涵项加上全程量词或者存在量词，那么它就成为全称命题或者特称命题了。1.1.1什

5、么是高级数理逻辑？高级数理逻辑是研究数理各种数理逻辑系统的构成和性质的科学。高级数理逻辑综合了数理逻辑、形式化方法和计算逻辑中的主要内容。主要内容包括：1、命题逻辑系统形式化描述2、一阶谓词逻辑系统形式化描述3、形式化系统的语义结构4、自动推理方法5、模态逻辑、时态逻辑6、非单调逻辑系统1.2数理逻辑发展1.2.1数理逻辑发展史逻辑学→数理逻辑→形式逻辑→计算逻辑1、逻辑思想的提出：亚里士多德提出建立探索人类推理、思维原则的学科，从而有了逻辑的概念。2、数理逻辑思想提出：莱布尼茨提出创造一种“通用的科学语言”，可以把推理过程

6、象数学一样利用公式来进行计算，从而得出正确的结论。由于当时的社会条件，他的想法并没有实现。但是它的思想却是现代数理逻辑部分内容的萌芽，从这个意义上讲，莱布尼茨的思想可以说是数理逻辑的先驱。1、数理逻辑诞生：1847年，英国数学家布尔发表了《逻辑的数学分析》，建立了“布尔代数”，并创造一套符号系统，利用符号来表示逻辑中的各种概念。布尔建立了一系列的运算法则，利用代数的方法研究逻辑问题，初步奠定了数理逻辑的基础。2、发展成独立学科：十九世纪末二十世纪初，数理逻辑有了比较大的发展，1884年，德国数学家弗雷格出版了《数论的基础》和

7、《符号论》，在书中引入量词的符号，使得数理逻辑的符号系统更加完备。对建立这门学科做出贡献的，还有美国人皮尔斯，他也在著作中引入了逻辑符号。从而使现代数理逻辑最基本的理论基础逐步形成，成为一门独立的学科。3、公理集合论促进了数理逻辑形式系统的产生：英国唯心主义哲学家、逻辑学家、数学家罗素在集合论的研究过程中，于1903年提出了著名的罗素悖论（数学史上的第三次危机）。罗素悖论动摇了集合论的基础，促使人们去研究数学中的矛盾性。从而提出了公里集合论。公里集合论的产生和发展，促进了形式系统的产生。德国数学家弗雷格《符号论》就是形式化系

8、统的原型。公里集合论促进了其他学科的发展，如罗巴契夫斯基几何的产生等。4、形式推理自动化的产生：1965年Robinson提出了归结原理（PrincipleofResolution），归结原理提出了基于形式描述的，利用计算机的推理方法。从而使机器定理证明和计算机辅助软件工程得到长足的发展。