历史

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

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

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

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

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

数理逻辑论的体系

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

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

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

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

一些基本结果

一些重要结果是：

一阶公式的普遍有效性的推定证明可用算法来检查有效性。用技术语言来说，证明集合是原始递归的。实质上，这就是哥德尔完全性定理，虽然那个定理的通常陈述使它与算法之间的关系不明显。

有效的一阶公式的集合是无限不可数（Uncountable Infinite）的。这一集合是“递归枚举的”，即不存在一图灵机（从而不存在任何现有计算机和算法）可以对某个非一阶公式的输入告诉你“这个输入一定不是一阶公式”——它可能一直运算下去。

普遍有效的二阶公式的集合甚至不是递归可枚举的。这是哥德尔不完全性定理的一个结果。

勒文海姆-斯科伦定理。

相继式演算中的切消定理。

保罗·约瑟夫·科恩（Paul Cohen）在1963年证明的连续统假设的独立性。

参考文献

A. S. Troelstra & H. Schwichtenberg (2000). Basic Proof Theory (Cambridge Tracts in Theoretical Computer Science) (2nd ed.). Cambridge University Press. ISBN 0-521-77911-1.

George Boolos & Richard Jeffrey (1989). Computability and Logic (3rd ed.). Cambridge University Press. ISBN 0-521-00758-5.

Elliott Mendelson (1997). Introduction to Mathematical Logic (4th ed.) Chapman & Hall.

A. G. Hamilton (1988). Logic for Mathematicians Cambridge University Press.

参见

逻辑

逻辑的语义

模型论

证明论

递归论

一阶逻辑

相继式演算

直觉主义逻辑

免责声明：以上内容版权归原作者所有，如有侵犯您的原创版权请告知，我们将尽快删除相关内容。感谢每一位辛勤著写的作者，感谢每一位的分享。