數理邏輯

出自 MBA智库百科(https://wiki.mbalib.com/)

　　數理邏輯是數學的一個分支，其研究對象是對證明和計算這兩個直觀概念進行符號化以後的形式系統。數理邏輯是數學基礎的一個不可缺少的組成部分。數理邏輯的研究範圍是邏輯中可被數學模式化的部分。以前稱為符號邏輯（相對於哲學邏輯），又稱元數學，後者的使用現已局限於證明論的某些方面。

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

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

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

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

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

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

　　程式語言學、語義學的研究從模型論衍生而來，而程式驗證中的模型檢測則從模型論衍生而來。柯里－霍華德同構給出了“證明”和“程式”的等價性，這一結果與證明論有關，直覺主義邏輯和線性邏輯在此起了很大作用。λ演算和組合子邏輯這樣的演算現在屬於理想程式語言。

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