绪论-课程简介.pptx

数理逻辑-课程简介马 帅北航计算机学fma@buaa.edu.cn吕江花计算机学院教师吕江花 软件开发环境国家重点实验室 北航新主楼G1135 jhlv@nlsde.buaa.edu.cn, jhlv@buaa.edu.cn 研究方向：软件形式化、软件自动化、安全攸关系统可信性研究。主要包括航空任务电子系统、航天器的可靠性验证等研究。助教： 孙梅莹博士后 乌尼日其其格博士 北航新主楼G1137数理逻辑 逻辑 研究思维形式及其推理规律的学科，探索、阐述 和确立有效推理原则 数理逻辑 用数学方法研究逻辑称为数理逻辑 即用数学符号体系研究逻辑，故又称之为 符号逻辑 史前时期古代希腊最伟大的哲学家，古典形式逻辑的创始人；在命题中引进了主谓项的变元，建立了三段论的理论；在逻辑史上第一次应用了形式化、公理化的的演绎系统，开创了逻辑的形式化研究；构造了模态三段论系统，开创了模态逻辑的研究；在《工具论》中，总结了正确的推理方法，建立了形式逻辑；在《分析篇》提出公理学理论的基础。亚里土多德(Aristotle，公元前384—322)传统逻辑传统逻辑主要是指亚里士多德逻辑经过中世纪的演变一直沿用到十九世纪;在中世纪被认为金科玉律、完美元缺;到了十九世纪，它的缺点突出，急需改革。传统逻辑主要缺点：传统逻辑所讨论的子句仅限于主宾式语句，分成四种：全称肯定A：Asp，凡s均为p；全称否定E，Esp，凡s均非p；特称肯定I，Isp，有的s为p；特称否定O，Osp；有的s非p。限于三段论。没有关于量词的研究，没有“变元”的概念。初创时期德国哲学家和数学家，17世纪末创建了数理逻辑。建立一种理想的“通用语言”进行推理。他曾经给一位友人的信上写道：“要是我少受搅扰，或者要是我更年青些，或有一些年青人来帮助我，我将作出一种 “通用代数”(在其中，一切推理的正确性将化归于计算．它同时又将是通用语言，但却和目前现有的一切语言完全不同；其中的字母和字将由推理来确定，除却事实的错误以外；所有的错误将只由于计算失误而来。要创作或发明这种语言或字母将是困难的，但要学习它，即使不用字典，也是很容易的。”莱布尼茨(Leibniz，1646—1716)初创时期德.摩根—关系逻辑19世纪英国数学家和逻辑学家，生于印度；1838年提出“数学归纳法”的概念；首先提出“论域”的概念，第一次明确用公式表达合取和析取的关系，称为德?摩根律；主张判断扩充为一般的关系语句，明确主张发展关系逻辑，逻辑代数的创始人之一。DeMorgan 1806-1871初创时期布尔—英国数学家1847年，发表了《逻辑的数学分析，论演绎推理演算》，1854年出版了《思维法则的探讨，作为逻辑与概率的数学理论的基础》建立了“布尔代数”，并创造一套符号系统，利用符号来表示逻辑中的各种概念，这是一种新的逻辑。建立了一系列的运算法则，利用代数的方法研究逻辑问题，初步奠定了数理逻辑的基础。George Boole 1815-1864初创时期皮尔斯C.S.Peirce1885年独立地引进了量词这个名称，以及存在量词?和全称量词两个符号。命题代数或命题演算．“既非…，又非”作为逻辑作为初始运算。在逻辑史上第一次全面、系统地建立了关系演算。皮尔斯和弗雷格都明确指出命题只有真假二值，命题的研究实质上是真假值的研究。Charles S. Peirce （1839-1914） 奠基时期弗雷格，德国人，数学家，逻辑学家，哲学家1879年的《表意符号》引入和使用量词与约束变元。1879年出版著作《概念文字：一种模仿算术语言构造的纯思维的形式语言》；第一次把谓词演算形式化,完备地发展了命题演算和谓词演算；历史上第一个严格的关于逻辑规律的公理系统；这个系统共有三个基本概念：蕴涵、否定和全称量词，共有九条公理。第一个引入了符号“├” ；接近于完成数理逻辑整个基础，标志着数理逻辑的发展由创建时期进入奠基时期。Gottlob Frege 1848-1925奠基时期皮亚诺，意大利数理逻辑学家；提出了自然数算术的一个公理系统1894年出版《数学公式》，逻辑符号体系沿用至今；用逻辑演算表述数学、推导数学；区分集合论中的“属于”关系和包含关系；关于自然数论的五个公理一直沿用到现在，成为自然数论的出发点。Giuseppe Peano 1858-1932奠基时期罗素，英国逻辑学家，哲学家；继承皮亚诺的研究，完备了命题演算和谓词演算的成果；以集合论为基础，给出了自然数定义，证明了自然数满足皮亚诺的五个公理；罗素总结了数理逻辑的成果，和怀特海合著了《数学原理》，他的成果汇集成为一本巨著，奠定了数理逻辑的基础。Bertrand Russell 1872-1970希尔柏特规划希尔柏特规划直接证明数学理论的相容性 数学理论公理化一一规