什么是数理逻辑 ■字面含义:数学理论的逻辑。逻辑是研 究演绎(推理)规律的学科。 广义理解:用数学方法研究演绎规律的 学科。 狭义理解:用数学方法研究数学中演绎 规律和数学基础的学科。 ■研究对象:推理过程的正确性标准。 是数学的一个分支。又称符号逻辑等
什么是数理逻辑 字面含义 : 数 学 理论的逻辑。逻辑是研 究演绎(推理)规律的学科。 广义理解:用数学方法研究演绎规律的 学科。 狭义理解:用数学方法研究数学中演绎 规律和数学基础的学科。 研究对象:推理过程的正确性标准。 是数学的一个分支。又称符号逻辑等
简单历史——三个阶段(一) 1.初始阶段:1660年代—19世纪末 将数学应用于逻辑 n Aristotle:形式逻辑(主词和谓词逻辑) 丶 Leibniz:建立直观而又精确的思维演算。 遇有争论,双方可以拿起笔来说:让我们 来算一下 George boole:,逻辑代数。 De morgan:关系逻辑。 1]王宪钧,数理逻辑引论,北京大学出版社,1982
简单历史——三个阶段(一) 1. 初始阶段:1660年代 — 19世纪末 将数学应用于逻辑 Aristotle:形式逻辑(主词和谓词逻辑)。 ¾ Leibniz:建立直观而又精确的思维演算。 遇有争论,双方可以拿起笔来说:让我们 来算一下。 ¾ George Boole: 逻辑代数。 ¾ De Morgan: 关系逻辑。 [1] 王宪钧,数理逻辑引论,北京大学出版社,1982
简单历史——三个阶段(二 2.过度阶段:19世纪末—1940前后 逻辑应用于数学 非欧几何与公理化方法。 微积分与实数理论, Piano算术。 集合论与数学基础(1900年世界数学家大会) 悖论与第三次数学危机,Hibe计划。 (第一次:勾股定理,无理数的发现) (第二次:穷小量是不是零?)
简单历史——三个阶段(二) 2. 过度阶段:19世纪末 — 1940前后 逻辑应用于数学 ¾ 非欧几何与公理化方法。 ¾ 微积分与实数理论,Piano算术。 ¾ 集合论与数学基础(1900年世界数学家大会) ¾ 悖论与第三次数学危机,Hilbert计划。 (第一次:勾股定理,无理数的发现) (第二次:穷小量是不是零?)
简单历史——三个阶段( ■成熟阶段:19305-1970年 成为数学的独立分支 Godel完全性定理和不完全性定理。 四个分支: 公理集合论:大基数,连续统问题 递归论(可计算性理论): Turing机,不可解性 模型论:实数的非标准模型 证明论:超穷归纳法, gentzen的数论和谐性证明
简单历史——三个阶段(三) 成熟阶段:1930s — 1970年 成为数学的独立分支 ¾ Gödel完全性定理和不完全性定理。 ¾ 四个分支: ¾ 公理集合论:大基数,连续统问题 ¾ 递归论(可计算性理论):Turing机,不可解性 ¾ 模型论:实数的非标准模型 ¾ 证明论:超穷归纳法, Gentzen的数论和谐性证明
特点与方法 公理化与形式化方法 ■特制的符号语言
特点与方法 公理化与形式化方法. 特制的符号语言
与计算机科学的联系 布尔电路:香龙 Shanon是第一人。 计算理论:可计算性, Turing机,形式语言,自动机, 计算复杂性。 程序语义与验证技术, Intel buc:5亿美元 程序的自动生成与转换。 SQL:本质上等价于一阶逻辑。 Prolog语言—以逻辑演算为基础 LTSP语言—以λ演算为基础 ■人工智能:非单调推理,缺省推理。 ■信息安全等
与计算机科学的联系 布尔电路:香龙Shanon是第一人。 计算理论:可计算性,Turing机,形式语言,自动机, 计算复杂性。 程序语义与验证技术. Intel bug: 5亿美元 。 程序的自动生成与转换。 SQL: 本质上等价于一阶逻辑。 Prolog语言——以逻辑演算为基础 LISP语言—— 以 λ演算为基础 人工智能:非单调推理,缺省推理。 信息安全等 ……
Dijkstra的话 我现在年纪大了,搞了这么多年软件,错 误不知犯了多少,现在觉悟了,我想,假 如我早年在数理逻辑上好好下点功夫的话, 我就不会犯这么多错误,不少东西逻辑学 家早就说了,可我不知道要是我能年轻20 岁的话我要回去学逻辑。 门]钱学森,关于思维科学的研究,思维科学,第3卷,1987。 [2]M.Y Vardi, a brief history of Logic, 2003
Dijkstra的话 我现在年纪大了,搞了这么多年软件,错 误不知犯了多少,现在觉悟了,我想,假 如我早年在数理逻辑上好好下点功夫的话, 我就不会犯这么多错误,不少东西逻辑学 家早就说了,可我不知道要是我能年轻20 岁的话我要回去学逻辑。 [1] 钱学森,关于思维科学的研究,思维科学,第3卷,1987。 [2] M. Y. Vardi, A Brief History of Logic, 2003
谢谢
谢 谢