簡介
數學邏輯（Mathematical logic）是與數學基礎，理論計算科學和哲學邏輯密切聯繫的一個數學分支。其研究對象包括邏輯的數學研究和把形式邏輯套用到數學的其它領域。數學邏輯統一主題包括研究形式系統的表現力和形式證明系統的推斷力。
數學邏輯的研究範圍是邏輯中可數學模式化的部分。以前稱為符號邏輯（相當於哲學邏輯）又稱元數學。現在，後者已局限於證明論的某些方面。
歷史
皮亞諾（Peano）首先提出“數學邏輯”的名稱。他又稱其為符號邏輯。數學邏輯的本質依然是亞里斯多德的邏輯學。但從記號學的觀點講，它是用抽象代數來記述的。
某些哲學傾向重的數學家用符號或代數方法來處理形式作過一些嘗試，比如說萊布尼茲·朗伯（JohannHeinrich Lambert）。但他們的工作鮮為人知，後繼無人。直到19世紀中頁，喬治·布爾和其後的奧古斯都·德·摩根才提出一種處理邏輯問題的系統性的數學方法（當然不是定量的）。亞里士多德以來的傳統邏輯有了定論，但這“新”邏輯在很大程度上澄清了有關數學問題。
傳統的數學研究較偏重於“論證的形式”，而當代數學邏輯的態度也許可被總結為對於內容的組合研究。它同時包括“語法”和“語義”。
數學邏輯的重要著作有哥特洛布·弗雷格（Gottlob Frege）的《概念文字》，伯特蘭·羅素的《數學原理》。
分支和領域
數學邏輯手冊對當代數學邏輯粗分為四個方面：
1.集合論
2.模擬論
3.遞歸論
4.證據理論和建設性數學
每個領域都有自已明顯的重點；雖然許多技術和結果多學科共享。這些學科間的界線以及數學邏輯與數學其它領域的界限常常不很清楚。哥德爾不完備性定理在遞歸理論和證據理論不僅是旅程碑，也導致模擬邏輯的Lob定律。強制法在集合論，模擬理論，和遞歸理論，以及直觀數學的研究中都有套用。
分類理論的數學領域用許多形式公理化方法，包括研究分類邏輯，但分類理論不考慮數學邏輯分支，因為它套用在不同數學領域，數學家們，包括Saunders Mac Lane已提議分類理論，獨立於集合論而為數學的基本系統。
形式邏輯系統
一階邏輯
一階邏輯是一種特別的邏輯形式系統。它的句法只包含有限形成的公式表達，而它的語義僅用有限的量詞在論述的有限範圍內代表。
其它經典邏輯
除一階邏輯外，還有許多邏輯，包括無限邏輯，它可用公式提供無限的信息。和高階邏輯。在它的語義中還包括一部分集合論。
非經典和模擬邏輯
模擬邏輯包括付加模擬運算元，例如一個運算元，陳述一個特別公式不僅真實，且要求真實.雖然模擬邏輯不常用到數學公理化，但它已用去研究一階可證的性質。
直覺邏輯
Heyting發展直覺邏輯去研究布勞威爾的直覺程式。直覺邏輯不包括排中定律，它的內容為：每個句子或它的反面是真的。Kleene直覺邏輯證明理論的工作指出：可從直覺邏輯的證明恢復建設性的信息。
代數邏輯
代數邏輯用抽象邏輯方法研究形式邏輯的語義。基本例是用布爾代數在經典命題邏輯中代表真值，而用Heyting代數在直覺命題邏輯中真值。如一階和高階更強邏輯則用如圓筒更複雜的代數結構。
集合理論
集合理論研究集，它是物體的抽象集合。許多基本觀念，如序和樞機主教數，是在形式集合理論前的主導者非正式發展的。由Zermelo第一個公理化稍為擴展，就變成了Zermolo-Fraenkelde1集合理論。它是現在數學最廣泛使用的基礎理論。
已有其它形式化的集合理論；包括Von Neumann-Bernays-Godel 集合理論，Morse-Kelley集合理論和新基礎。
模擬理論
模擬理論研究各種形式理論的模型。特別形式邏輯集合理論的公式集合，模擬理論用結構對集合理論作具體的解析模擬理論與泛代數和代數幾何有密切關係，雖然模擬理論的方法較它們更集中考慮邏輯。
特別理論所有模型的集合稱為元素類。經典模擬理論尋求決定特別元素類內模型的基本性質或決定是否某結構類形成元素類。
遞歸理論
遞歸理論，也稱可計算理論，研究可計算函式和圖靈度，它把不可計算函式分為有相同不可計算程度的集，遞歸理論也包括研究一般化可計算性和可定義性。遞歸理論由1930年Alonzo Church 和Alan Turing的工作發展，1940年，Kleene和Post做了很大擴展。
算法不可解問題
遞歸理論一個重要分支研究算法的不可解性；如不可能計算而對所有合理輸入返回正確答案，這就是一個決策問題或函式問題是算法不可解問題。1936年Church 和Turing所獨立第一次得到關於不可解的結果顯示，Entscheidung問題是算法不可解問題。
