PROFILBARU.COM

数理逻辑（英語：Mathematical logic）是数学的一个分支，其研究对象是对证明和计算这两个直观概念进行符号化以后的形式系统。数理逻辑是数学基础的一个不可缺少的组成部分。主要的子研究领域有模型论，证明论，集合论和可计算性理论。

数理逻辑的研究范围是逻辑中可被数学模式化的部分。以前称为符号逻辑（相对于哲学逻辑），又称元数学。数理逻辑一般着重于研究公理系统的推断能力和表达能力。它也包括分析正确的数学推断来构筑数学基础。

研究内容

数理逻辑的主要分支包括：

有时候计算复杂性理论也会被认为是数理逻辑的一部分。

每个分支都有着重研究的方向,但是很多结论是共享的,分支和分支之间的界限不是非常严格。

比如哥德尔不完备定理不仅仅是证明论和递归论的重大成果,它还直接影响了模型论中的勒布定理(Löb's theorem). 因为都基于公理化集合论,数理逻辑的不同分支的证明方法也有相通之处，比如力迫可以用来研究模型论,递归论和证明论。

范畴论也是和数理逻辑有关的数学分支，范畴论的证明方法使用许多公理化的证明方式，但因为其在数学中的广阔应用范围，往往被认为是一个独立的分支。这两个学科的直接联系是范畴逻辑. 但也有范畴论方面的数学家，桑德斯·麦克莱恩认为范畴论独立于集合论也构成了数学基础。这个观点基于拓扑斯理论。

与计算机科学的关系

数理逻辑和计算机科学尤其是理论计算机科学有许多重合之处，许多计算机科学的先驱者既是数学家、又是逻辑学家，如哥德尔、艾倫·圖靈、邱奇、克劳德·香农、斯蒂芬·科尔·克莱尼等。

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

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

与之相应的，计算机科学在自动验证和自动寻找证明等技巧方面的成果对逻辑研究做出了反哺，比如说自动定理证明、计算机辅助证明、计算群论和逻辑编程的应用。

历史

早期历史

逻辑史

十八世纪

某些哲学倾向浓厚的数学家对用符号或代数方法来处理形式逻辑作过一些尝试，比如说莱布尼兹和朗伯（Johann Heinrich Lambert）。莱布尼茨的演算推论器（英语：Calculus ratiocinator），很能让人想起符号逻辑，可以被看作使这种计算成为可行的一种方式。但他们的工作鲜为人知，后继无人。

十九世纪

数理逻辑的概念在十九世纪中期出现了，它是两个古老的学科：数学和哲学逻辑的交汇。^[1] 数理逻辑被称之为符号逻辑或形式逻辑或者逻辑代数。“数理逻辑”的名称是由皮亚诺首先给出，数理逻辑在本质上依然是亚里士多德的逻辑学，但相比于古典哲学中只运用修辞学，直言三段论和哲学的方法，数理逻辑使用更为严格的推断和借用了很多抽象代数的符号来记述。^[2]^[3]

十九世纪初，乔治·布尔和稍后的奥古斯都·德·摩根都提出了一种处理逻辑问题的系统性的数学方法，但没有使用量化 (数理逻辑)。

戈特洛布·弗雷格1879年出版了一本关于逻辑学的书《概念文字》。书的完整标题为《模仿算术的纯思维的形式语言》。这本书被认为无可争议是亚里士多德之后在逻辑学领域最重要的出版物。弗雷格开发他的形式逻辑系统的动机是类似于莱布尼兹对“演算推论器（英语：Calculus ratiocinator）”的渴望。演算加入了量词，因而本质上是经典的谓词逻辑。

在逻辑中，算术一词指的是关于自然数的理论。朱塞佩·皮亚诺提出了一套以他的名字命名的算术公理皮亚诺公理。这套公理系统使用布尔和薛定谔逻辑系统的变体，并且添加了量化 (数理逻辑)的概念。皮亚诺当时并不知道戈特洛布·弗雷格所做的相似工作。

大约在同一时间，理查德·戴德金证明了自然数具有归纳的独特特征。戴德金提出了一种不同的证明思路，这种证明缺乏皮亚诺公理的形式逻辑特征。然而，戴德金的工作证明了皮亚诺系统中无法证明的定理，包括自然数集合的唯一性（考虑同构的情况下）以及函数和数学归纳的加法和乘法的递归定义。亚里士多德以来的传统逻辑得到改革和完成，数学家也由此得到了研究数学基本概念的合适工具。虽然这并不意味着1900年至1925年间的有关数学基础的争论已有了定论，但这“新”逻辑在很大程度上澄清了有关数学的哲学问题。

二十世纪

二十世纪前叶，因为关于数学基础的几次大辩论，数理逻辑迎来了基础理论学术产出的大爆炸。

二十一世纪

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

一些基本结果

一些重要结果是：

一阶公式的普遍有效性的推定证明可用算法来检查有效性。用技术语言来说，证明集合是原始递归的。实质上，这就是哥德尔完全性定理，虽然那个定理的通常陈述使它与算法之间的关系不明显。
有效的一阶公式的集合是不可计算的，也就是说，不存在算法用作检测一條公式是否普遍成立。不過，儘管一階邏輯不可判定，仍是“半可判定”的，即存在某個算法，滿足：对此算法输入一个一阶公式，如果这个一阶公式是普遍有效的，那么算法将在某一时刻停机；如果不是普遍有效的，那么算法将会永远不停地计算下去。然而，即使算法已经运行了亿万年，仍無法分辨公式是否有效。换句话说，有效公式的集合是“递归可枚举集合”。
普遍有效的二阶公式的集合甚至不是递归可枚举的。这是哥德尔不完全性定理的一个结果。
勒文海姆-斯科伦定理。
相继式演算中的切消定理。
保罗·约瑟夫·科恩（Paul Cohen）在1963年证明的连续统假设的独立性。

参见

參考資料

^ Ferreirós, José. The Road to Modern Logic-An Interpretation (PDF). Bulletin of Symbolic Logic.: 441–484. [2023-01-24]. doi:10.2307/2687794. （原始内容存档 (PDF)于2023-02-02）.
^ Bochenski,Jozef Maria; Translated by Otto Bird. Calculationes Suiseth Anglici (in Lithuanian). Springer. 1959. ISBN 9789048183286 请检查|isbn=值 (帮助).
^ Swinehead,Richard. Calculationes Suiseth Anglici (in Lithuanian). Calculationes Suiseth Anglici (in Lithuanian). 1498.

A. S. Troelstra（英语：A. S. Troelstra） & H. Schwichtenberg（英语：Helmut Schwichtenberg） (2000). Basic Proof Theory (Cambridge Tracts in Theoretical Computer Science) (2nd ed.). Cambridge University Press. ISBN 0-521-77911-1.
George Boolos（英语：George Boolos） & Richard Jeffrey（英语：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.