数理逻辑
数理逻辑（英语：Mathematical logic），数学的一个分支，是用数学的方法研究逻辑推理和数学计算，将推理论证、数学计算的过程符号化、形式化、公理化的学科。其研究对象是对证明和计算这两个直观概念进行符号化以后的形式系统。数理逻辑是数学基础的一个不可缺少的组成部分。
数理逻辑的研究范围是逻辑中可被数学模式化的部分。以前称为符号逻辑（相对于哲学逻辑），又称元数学，后者的使用现已局限于证明论的某些方面。
概述
17世纪中叶，德国数学家莱布尼茨设想建立一种用符号语言表示，能像数学证明一样进行的思维演算。直到19世纪初，英国数学家布尔成功地构造一种能够反映逻辑运算的代数结构——布尔代数，初步实现莱布尼茨的设想。代数方法和传统逻辑结合产生了命题演算。
早在公元前3世纪，希腊数学家欧几里得编写的《几何原本》就采用5条不加证明的命题作公理和公设，其他所有定理都是用这5条公理公设推理得到。历史上不少数学家试图用这5条中的其他公理公设来证明欧几里得第五公设，历经一千多年没有成功。19世纪中叶，俄国数学家罗巴切夫斯基不用欧几里得第五公设，而假定三角形内角和小于180°，得到第一个非欧几里得几何，称为罗巴切夫斯基几何（见非欧几里得几何学）。德国数学家黎曼假定三角形内角和大于180°，得到另一种非欧几里得几何，称为黎曼几何。19世纪末，德国数学家希尔伯特给出简单而完全的由20条公理组成的公理化的欧几里得几何系统，并用实数算术理论为它建立了一个模型。几何公理化的同时，分析学和代数学也都走向公理化。
19世纪末，德国数学家弗雷格把数学中的函数概念、量词和约束变元引进逻辑系统，建立第一个公理化的谓词演算系统。20世纪初，英国数学家罗素和怀特海合著的《数学原理》出版，标志数理逻辑的基础——命题演算和谓词演算的发展已经相当完善。
19世纪70年代，德国数学家康托尔研究了超穷基数和序数的性质，用一一对应方法对无穷集合进行分类，并在此基础上建立了集合论。康托尔的集合论受到数学家赞誉，称为数学的基础。1901年，年轻的罗素依据康托尔定义集合的方法给出“一切不属于自己的集合组成的集合”的集合定义，用符号表示为A={X：XX}。然而这个集合引起逻辑矛盾：A∈A当且仅当AA。这一矛盾动摇了集合论的整个基础，也动摇了整个数学的基础。为了挽救这一危机，数学家和逻辑学家做了大量工作，展开了激烈辩论，逐步形成三个主要学派。
以罗素为代表的逻辑主义学派，认为数学的基础是逻辑，主张用逻辑推演出全部数学。为了避免悖论，罗素提出“分支类型论”，把集合分成不同层次，每个集合属于一个层次，集合内部的元素属于较低的层次。这样每个集合都不能是自己的元素。但逻辑主义把数学变得非常复杂，没有给出完备的公理体系，终未能为大多数数学家接受。
以荷兰数学家L.E.J.布劳威尔为代表的直觉主义学派，主张数学的对象及真理应当能够通过数学的理性或直觉的活动而直接得到。他排斥一切非构造性的证明，认为任何一个数学对象，必须能行地构造出来，而不能用反证法推出其存在。这样直觉主义不承认排中律p∨﹁p，﹁﹁p→p。布劳威尔及其追随者以复杂的构造为代价，重建了大部分数学。直觉主义数学构造非常复杂，不容易得到认可，但他们的构造性证明，在计算机科学中有相当重要的意义。
以希尔伯特为代表的形式构造学派，主张把数学严格形式化，构造各式各样的形式体系，每个体系各自构成特有的逻辑和数学内容。希尔伯特制定了一整套方案用来证明形式系统的不矛盾性。他捍卫排中律，但只允许用有穷长的证明。他承认潜无穷，但涉及潜无穷时不使用排中律。
20世纪初数学基础的研究，极大地推动了数理逻辑的发展。1931年K.哥德尔的不完全性定理的出现，使希尔伯特寻找形式系统一致性证明的方案归于失败。正是哥德尔的工作，使现代逻辑发生革命性的变化。哥德尔开创了数理逻辑迅速发展的新时期。
哥德尔的不完全性定理发表以来，数理逻辑出现四大分支：公理集合论、模型论、递归论和证明论，构成数理逻辑的主要内容，它们都已发展成为数学中独立的分支。数理逻辑也因此成为数学逻辑。除此之外，由于各种应用而产生的非经典逻辑层出不穷，如模态逻辑、时态逻辑、概率逻辑等，它们都被认为是数理逻辑的组成部分。
数理逻辑已经成为计算机科学的基础，计算机线路设计、计算机程序设计、编译系统、计算机算法及其复杂性、数据库、计算机控制、人工智能等都离不开数理逻辑。与计算机有关的逻辑系统也层出不穷。另外，数理逻辑在其他数学分支中的应用也越来越多，如解决了希尔伯特第1问题和第10问题，以及代数学、拓扑学、分析学中的不少难题。
历史
“数理逻辑”的名称由皮亚诺首先给出，他又称其为符号逻辑或形式逻辑。数理逻辑在本质上依然是亚里士多德的逻辑学，但从记号学的观点来讲，它是用抽象代数来记述的。
某些哲学倾向浓厚的数学家对用符号或代数方法来处理形式逻辑作过一些尝试，比如说莱布尼兹和朗伯（Johann Heinrich Lambert）；但他们的工作鲜为人知，后继无人。直到19世纪中叶，乔治·布尔和其后的奥古斯都·德·摩根才提出了一种处理逻辑问题的系统性的数学方法（当然不是定量性的）。
亚里士多德以来的传统逻辑得到改革和完成，由此也得到了研究数学基本概念的合适工具。虽然这并不意味着1900年至1925年间的有关数学基础的争论已有了定论，但这“新”逻辑在很大程度上澄清了有关数学的哲学问题。
传统的逻辑研究（参见逻辑论题列表）较偏重于“论证的形式”，而当代数理逻辑的态度也许可以被总结为对于内容的组合研究。它同时包括“语法”（例如，从一形式语言把一个文字串传送给一编译器程序，从而转写为机器指令）和“语义”（在模型论中构造特定模型或全部模型的集合）。
数理逻辑的重要著作有戈特洛布·弗雷格（Gottlob Frege）的《概念文字》（Begriffsschrift）、伯特兰·罗素的《数学原理》（Principia Mathematica）等。
数理逻辑论的体系
数理逻辑的主要分支包括：模型论、证明论、递归论和公理化集合论。数理逻辑和计算机科学有许多重合之处，这是因为许多计算机科学的先驱者既是数学家、又是逻辑学家，如艾伦·图灵、邱奇等。
程序语言学、语义学的研究从模型论衍生而来，而程序验证中的模型检测则从模型论衍生而来。
柯里－霍华德同构给出了“证明”和“程序”的等价性，这一结果与证明论有关，直觉主义逻辑和线性逻辑在此起了很大作用。λ演算和组合子逻辑这样的演算现在属于理想程序语言。
计算机科学在自动验证和自动寻找证明等技巧方面的成果对逻辑研究做出了贡献，比如说自动定理证明和逻辑编程。
一些基本结果
一些重要结果是：
- 一阶公式的普遍有效性的推定证明可用算法来检查有效性。用技术语言来说，证明集合是原始递归的。实质上，这就是哥德尔完全性定理，虽然那个定理的通常陈述使它与算法之间的关系不明显。
- 有效的一阶公式的集合是不可计算的，也就是说，不存在算法用作检测一条公式是否普遍成立。不过，尽管一阶逻辑不可判定，仍是“半可判定”的，即存在某个算法，满足：对此算法输入一个一阶公式，如果这个一阶公式是普遍有效的，那么算法将在某一时刻停机；如果不是普遍有效的，那么算法将会永远不停地计算下去。然而，即使算法已经运行了亿万年，仍无法分辨公式是否有效。换句话说，有效公式的集合是“递归可枚举集合”。
- 普遍有效的二阶公式的集合甚至不是递归可枚举的。这是哥德尔不完全性定理的一个结果。
- 勒文海姆-斯科伦定理。
- 相继式演算中的切消定理。
- 保罗·约瑟夫·科恩（Paul Cohen）在1963年证明的连续统假设的独立性。
参见
→ 学科目录： 哲学（目录）
