Remove ads
數理邏輯（英語：Mathematical logic）是數學的一個分支，其研究對象是對證明和計算這兩個直觀概念進行符號化以後的形式系統。數理邏輯是數學基礎的一個不可缺少的組成部分。主要的子研究領域有模型論，證明論，集合論和可計算性理論。
 | 此條目需要補充更多來源。 (2024年6月13日) |
數理邏輯的研究範圍是邏輯中可被數學模式化的部分。以前稱為符號邏輯（相對於哲學邏輯），又稱元數學。數理邏輯一般著重於研究公理系統的推斷能力和表達能力。它也包括分析正確的數學推斷來構築數學基礎。
數理邏輯的主要分支包括：
有時候計算複雜性理論也會被認為是數理邏輯的一部分。
每個分支都有著重研究的方向,但是很多結論是共享的,分支和分支之間的界限不是非常嚴格。
比如哥德爾不完備定理不僅僅是證明論和遞歸論的重大成果,它還直接影響了模型論中的勒布定理(Löb's theorem). 因為都基於公理化集合論,數理邏輯的不同分支的證明方法也有相通之處，比如力迫可以用來研究模型論,遞歸論和證明論。
範疇論也是和數理邏輯有關的數學分支，範疇論的證明方法使用許多公理化的證明方式，但因為其在數學中的廣闊應用範圍，往往被認為是一個獨立的分支。這兩個學科的直接聯繫是範疇邏輯. 但也有範疇論方面的數學家，桑德斯·麥克萊恩認為 範疇論獨立於集合論也構成了數學基礎。這個觀點基於拓撲斯理論。
數理邏輯和計算機科學尤其是理論計算機科學有許多重合之處，許多計算機科學的先驅者既是數學家、又是邏輯學家，如哥德爾、艾倫·圖靈、邱奇、克勞德·香農、史蒂芬·科爾·克萊尼等。
計算機科學中的程序語言學、語義學的研究從模型論衍生而來，而程序驗證中的模型檢測則從模型論衍生而來。
柯里－霍華德同構給出了「證明」和「程序」的等價性，這一結果與證明論有關，直覺主義邏輯和線性邏輯在此起了很大作用。λ演算和組合子邏輯的演算屬於理想的程序語言。
與之相應的，計算機科學在自動驗證和自動尋找證明等技巧方面的成果對邏輯研究做出了反哺，比如說自動定理證明、計算機輔助證明、計算群論和邏輯編程的應用。
某些哲學傾向濃厚的數學家對用符號或代數方法來處理形式邏輯作過一些嘗試，比如說萊布尼茲和朗伯（Johann Heinrich Lambert）。萊布尼茨的演算推論器，很能讓人想起符號邏輯，可以被看作使這種計算成為可行的一種方式。但他們的工作鮮為人知，後繼無人。
數理邏輯的概念在十九世紀中期出現了，它是兩個古老的學科：數學和哲學邏輯的交匯。[1] 數理邏輯被稱之為符號邏輯或形式邏輯或者邏輯代數。「數理邏輯」的名稱是由皮亞諾首先給出，數理邏輯在本質上依然是亞里斯多德的邏輯學，但相比於古典哲學中只運用修辭學，直言三段論和哲學的方法，數理邏輯使用更為嚴格的推斷和借用了很多抽象代數的符號來記述。[2][3]
十九世紀初，喬治·布爾和稍後的奧古斯都·德·摩根都提出了一種處理邏輯問題的系統性的數學方法，但沒有使用量化 (數理邏輯)。
戈特洛布·弗雷格1879年出版了一本關於邏輯學的書《概念文字》。書的完整標題為《模仿算術的純思維的形式語言》。這本書被認為無可爭議是亞里斯多德之後在邏輯學領域最重要的出版物。弗雷格開發他的形式邏輯系統的動機是類似於萊布尼茲對「演算推論器」的渴望。演算加入了量詞，因而本質上是經典的謂詞邏輯。
在邏輯中，算術一詞指的是關於自然數的理論。朱塞佩·皮亞諾提出了一套以他的名字命名的算術公理皮亞諾公理。這套公理系統使用布爾和薛丁格邏輯系統的變體，並且添加了量化 (數理邏輯)的概念。皮亞諾當時並不知道戈特洛布·弗雷格所做的相似工作。
大約在同一時間，理察·戴德金證明了自然數具有歸納的獨特特徵。戴德金提出了一種不同的證明思路，這種證明缺乏皮亞諾公理的形式邏輯特徵。然而，戴德金的工作證明了皮亞諾系統中無法證明的定理，包括自然數集合的唯一性（考慮同構的情況下）以及函數和數學歸納的加法和乘法的遞歸定義。 亞里斯多德以來的傳統邏輯得到改革和完成，數學家也由此得到了研究數學基本概念的合適工具。雖然這並不意味著1900年至1925年間的有關數學基礎的爭論已有了定論，但這「新」邏輯在很大程度上澄清了有關數學的哲學問題。
Remove ads
二十世紀前葉，因為關於數學基礎的幾次大辯論，數理邏輯迎來了基礎理論學術產出的大爆炸。
傳統的邏輯研究（參見邏輯論題列表）較偏重於「論證的形式」，而當代數理邏輯的態度也許可以被總結為對於內容的組合研究。它同時包括「語法」（例如，從一形式語言把一個文字串傳送給一編譯器程序，從而轉寫為機器指令）和「語義」（在模型論中構造特定模型或全部模型的集合）。
一些重要結果是：
- 一階公式的普遍有效性的推定證明可用算法來檢查有效性。用技術語言來說，證明集合是原始遞歸的。實質上，這就是哥德爾完全性定理，雖然那個定理的通常陳述使它與算法之間的關係不明顯。
- 有效的一階公式的集合是不可計算的，也就是說，不存在算法用作檢測一條公式是否普遍成立。不過，儘管一階邏輯不可判定，仍是「半可判定」的，即存在某個算法，滿足：對此算法輸入一個一階公式，如果這個一階公式是普遍有效的，那麼算法將在某一時刻停機；如果不是普遍有效的，那麼算法將會永遠不停地計算下去。然而，即使算法已經運行了億萬年，仍無法分辨公式是否有效。換句話說，有效公式的集合是「遞歸可枚舉集合」。
- 普遍有效的二階公式的集合甚至不是遞歸可枚舉的。這是哥德爾不完全性定理的一個結果。
- 勒文海姆-斯科倫定理。
- 相繼式演算中的切消定理。
- 保羅·約瑟夫·科恩（Paul Cohen）在1963年證明的連續統假設的獨立性。
數理邏輯的重要著作有戈特洛布·弗雷格（Gottlob Frege）的《概念文字》（Begriffsschrift）、伯特蘭·羅素的《數學原理》（Principia Mathematica）等。
Wikiwand in your browser!
Seamless Wikipedia browsing. On steroids.
Every time you click a link to Wikipedia, Wiktionary or Wikiquote in your browser's search results, it will show the modern Wikiwand interface.
Wikiwand extension is a five stars, simple, with minimum permission required to keep your browsing private, safe and transparent.
Remove ads