数理逻辑

维基百科,自由的百科全书
跳转至: 导航搜索

数理逻辑数学的一个分支,其研究对象是对证明计算这两个直观概念进行符号化以后的形式系统。数理逻辑是数学基础的一个不可缺少的组成部分。

数理逻辑的研究范围是逻辑中可被数学模式化的部分。以前称为符号逻辑(相对于哲学逻辑),又称元数学,后者的使用现已局限于证明论的某些方面。

历史[编辑]

“数理逻辑”的名称由皮亚诺首先给出,他又称其为符号逻辑。数理逻辑在本质上依然是亚里士多德的逻辑学,但从记号学的观点来讲,它是用抽象代数来记述的。

某些哲学倾向浓厚的数学家对用符号或代数方法来处理形式逻辑作过一些尝试,比如说莱布尼兹朗伯(Johann Heinrich Lambert);但他们的工作鲜为人知,后继无人。直到19世纪中叶,乔治·布尔和其后的奥古斯都·德·摩根才提出了一种处理逻辑问题的系统性的数学方法(当然不是定量性的)。

亚里士多德以来的传统逻辑得到改革和完成,由此也得到了研究数学基本概念的合适工具。虽然这并不意味着1900年至1925年间的有关数学基础的争论已有了定论,但这“新”逻辑在很大程度上澄清了有关数学的哲学问题

传统的逻辑研究(参见逻辑论题列表)较偏重于“论证的形式”,而当代数理逻辑的态度也许可以被总结为对于内容的组合研究。它同时包括“语法”(例如,从一形式语言把一个文字串传送给一编译器程序,从而转写为机器指令)和“语义”(在模型论中构造特定模型或全部模型的集合)。

数理逻辑的重要著作有哥特洛布·弗雷格(Gottlob Frege)的《概念文字》(Begriffsschrift)、伯特兰·罗素的《数学原理》(Principia Mathematica)等。

数理逻辑论的体系[编辑]

数理逻辑的主要分支包括:模型论证明论递归论公理化集合论。数理逻辑和计算机科学有许多重合之处,这是因为许多计算机科学的先驱者既是数学家、又是逻辑学家,如阿兰·图灵邱奇等。

程序语言学语义学的研究从模型论衍生而来,而程序验证中的模型检测则从模型论衍生而来。

柯里-霍华德同构给出了“证明”和“程序”的等价性,这一结果与证明论有关,直觉主义逻辑线性逻辑在此起了很大作用。λ演算组合子逻辑这样的演算现在属于理想程序语言

计算机科学在自动验证和自动寻找证明等技巧方面的成果对逻辑研究做出了贡献,比如说自动定理证明逻辑编程

一些基本结果[编辑]

一些重要结果是:

  • 一阶公式的普遍有效性的推定证明可用算法来检查有效性。用技术语言来说,证明集合是原始递归的。实质上,这就是哥德尔完全性定理,虽然那个定理的通常陈述使它与算法之间的关系不明显。
  • 有效的一阶公式的集合是无限不可数(Uncountable Infinite)的。这一集合是“递归枚举的”,即不存在一图灵机(从而不存在任何现有计算机和算法)可以对某个非一阶公式的输入告诉你“这个输入一定不是一阶公式”——它可能一直运算下去。

参考文献[编辑]

外部链接[编辑]

参见[编辑]