數理邏輯

數理邏輯（英語：Mathematical logic）是數學的一個分支，其研究對象是對證明和計算這兩個直觀概念進行符號化以後的形式系統。數理邏輯是數學基礎的一個不可缺少的組成部分。

數理邏輯的研究範圍是邏輯中可被數學模式化的部分。以前稱為符號邏輯（相對於哲學邏輯），又稱元數學，後者的使用現已局限於證明論的某些方面。

歷史

「數理邏輯」的名稱由皮亞諾首先給出，他又稱其為符號邏輯。數理邏輯在本質上依然是亞里斯多德的邏輯學，但從記號學的觀點來講，它是用抽象代數來記述的。

某些哲學傾向濃厚的數學家對用符號或代數方法來處理形式邏輯作過一些嘗試，比如說萊布尼茲和朗伯（Johann Heinrich Lambert）；但他們的工作鮮為人知，後繼無人。直到19世紀中葉，喬治·布爾和其後的奧古斯都·德·摩根才提出了一種處理邏輯問題的系統性的數學方法（當然不是定量性的）。

亞里斯多德以來的傳統邏輯得到改革和完成，由此也得到了研究數學基本概念的合適工具。雖然這並不意味著1900年至1925年間的有關數學基礎的爭論已有了定論，但這「新」邏輯在很大程度上澄清了有關數學的哲學問題。

傳統的邏輯研究（參見邏輯論題列表）較偏重於「論證的形式」，而當代數理邏輯的態度也許可以被總結為對於內容的組合研究。它同時包括「語法」（例如，從一形式語言把一個文字串傳送給一編譯器程序，從而轉寫為機器指令）和「語義」（在模型論中構造特定模型或全部模型的集合）。

數理邏輯的重要著作有戈特洛布·弗雷格（Gottlob Frege）的《概念文字》（Begriffsschrift）、伯特蘭·羅素的《數學原理》（Principia Mathematica）等。

數理邏輯的主要分支包括：模型論、證明論、遞歸論和公理化集合論。數理邏輯和計算機科學有許多重合之處，這是因為許多計算機科學的先驅者既是數學家、又是邏輯學家，如艾倫·圖靈、邱奇等。

程序語言學、語義學的研究從模型論衍生而來，而程序驗證中的模型檢測則從模型論衍生而來。

柯里－霍華德同構給出了「證明」和「程序」的等價性，這一結果與證明論有關，直覺主義邏輯和線性邏輯在此起了很大作用。λ演算和組合子邏輯這樣的演算現在屬於理想程序語言。

計算機科學在自動驗證和自動尋找證明等技巧方面的成果對邏輯研究做出了貢獻，比如說自動定理證明和邏輯編程。

一些重要結果是：

一階公式的普遍有效性的推定證明可用算法來檢查有效性。用技術語言來說，證明集合是原始遞歸的。實質上，這就是哥德爾完全性定理，雖然那個定理的通常陳述使它與算法之間的關係不明顯。
有效的一階公式的集合是不可計算的，也就是說，不存在算法用作檢測一條公式是否普遍成立。不過，儘管一階邏輯不可判定，仍是「半可判定」的，即存在某個算法，滿足：對此算法輸入一個一階公式，如果這個一階公式是普遍有效的，那麼算法將在某一時刻停機；如果不是普遍有效的，那麼算法將會永遠不停地計算下去。然而，即使算法已經運行了億萬年，仍無法分辨公式是否有效。換句話說，有效公式的集合是「遞歸可枚舉集合」。
普遍有效的二階公式的集合甚至不是遞歸可枚舉的。這是哥德爾不完全性定理的一個結果。
勒文海姆-斯科倫定理。
相繼式演算中的切消定理。
保羅·約瑟夫·科恩（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.