数理逻辑（英语：mathematical logic），用数学的方法研究逻辑推理和数学计算，将推理论证、数学计算的过程符号化、形式化、公理化的学科。数学的分支。又称符号逻辑、数学逻辑。相对于2,000多年前已建立的古典形式逻辑而言，又称现代逻辑。
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问题，以及代数学、拓扑学、分析学中的不少难题。
