數學邏輯
數學邏輯是數學中形式邏輯的研究。主要的次序包括模型理論，證明理論，集合理論和遞歸理論（也稱為可計算理論）。數學邏輯中的研究通常涉及形式邏輯系統的數學特性，例如其表現力或演繹能力。但是，它還可以包括使用邏輯來表徵正確的數學推理或建立數學基礎。
自成立以來，數學邏輯既促成了數學基礎的研究，也促進了數學邏輯。這項研究始於19世紀後期，發展了用於幾何，算術和分析的公理框架。在20世紀初期，戴維·希爾伯特（David Hilbert ）的計劃塑造了基礎理論的一致性。 KurtGödel ， Gerhard Gentzen等人的結果為該計劃提供了部分解決方案，並闡明了證明一致性所涉及的問題。集合理論中的工作表明，幾乎所有普通的數學都可以通過集合形式化，儘管有些定理在共同的公理系統中無法證明集合理論。數學基礎中的當代工作通常集中於確定可以在特定正式系統（如相反的數學中）形式化數學的哪些部分，而不是試圖找到可以開發所有數學的理論。
子場和範圍
1977年的數學邏輯手冊將當代數學邏輯的粗略劃分為四個領域：
另外，有時計算複雜性理論的領域也被包括在數學邏輯的一部分。每個區域都有明顯的重點，儘管許多技術和結果在多個領域共享。這些領域之間的邊界線以及分隔數學邏輯和其他數學領域的線並不總是清晰的。戈德爾的不完整定理不僅標誌著遞歸理論和證明理論中的一個里程碑，而且還導致了模態邏輯中的Löb定理。強迫的方法用於集合理論，模型理論和遞歸理論，以及直覺數學的研究。
類別理論的數學領域使用了許多形式的公理方法，其中包括對分類邏輯的研究，但是類別理論通常不被視為數學邏輯的子場。由於它在數學領域的適用性，包括桑德斯·麥克巷（Saunders Mac Lane）在內的數學家將類別理論作為數學的基礎系統提出，獨立於集合理論。這些基金會使用的座椅類似於可能採用經典或非經典邏輯的集合理論的通用模型。
歷史
數學邏輯在19世紀中葉出現為數學子場，反映了兩種傳統的融合：正式的哲學邏輯和數學。 “數學邏輯，也稱為'logistic'，'符號邏輯'，'邏輯代數'，最近，簡單地簡單地“正式邏輯”，是上一個十九世紀的邏輯理論的集合。輔助人造符號和嚴格的演繹方法。”在這種出現之前，通過修辭學，計算，三段論和哲學對邏輯進行了研究。 20世紀上半葉，基本結果發生了爆炸，伴隨著關於數學基礎的激烈辯論。
早期歷史
邏輯理論是在許多歷史文化中發展的，包括中國，印度，希臘和伊斯蘭世界。希臘方法，特別是Organon中發現的亞里士多德邏輯（或術語邏輯），在西方科學和數學中發現了廣泛的應用和接受。 Stoics ，尤其是Chrysippus ，開始了謂語邏輯的發展。在18世紀的歐洲，試圖以像徵性或代數的方式來治療正式邏輯的運作，包括萊布尼茲和蘭伯特在內的哲學數學家，但他們的勞動仍然孤立，鮮為人知。
19世紀
在19世紀中葉，喬治·布爾（George Boole）和奧古斯都·德·摩根（Augustus de Morgan）介紹了邏輯的系統數學處理。他們的工作是基於喬治·孔雀等代數主義者的工作，將傳統的亞里士多德邏輯學說擴展到了一個足夠的框架，以研究數學基礎。 1847年。瓦特羅斯拉夫·貝蒂奇（VatroslavBertić）在邏輯的代數化方面進行了實質性工作，獨立於布爾。查爾斯·桑德斯·皮爾斯（Charles Sanders Peirce）後來建立在布爾（Boole）的工作中，以開發一種用於關係和量詞的邏輯系統，他在1870年至1885年的幾篇論文中發表了該系統。
Gottlob Frege在1879年出版的Begriffsschrift中用量化詞進行了獨立的邏輯發展，該作品通常被認為是邏輯史上的轉折點。然而，弗雷格的作品仍然晦澀難懂，直到伯特蘭·羅素（Bertrand Russell）在世紀之交開始推廣。弗雷格（Frege）開發的二維符號從未被廣泛採用，在當代文本中未使用。
從1890年到1905年，恩斯特·施羅德（ErnstSchröder）在三卷中出版了vorlesungenüber模具代數logik 。這項工作總結並擴展了Boole，de Morgan和Peirce的工作，並全面提及了象徵性邏輯，正如19世紀末所理解的那樣。
基礎理論
擔心數學尚未建立在適當的基礎上，從而導致為數學基本領域（例如算術，分析和幾何形狀）的基本領域的發展開發。
在邏輯上，算術一詞是指自然數的理論。 Giuseppe Peano使用Boole和Schröder的邏輯系統的變體出版了算法（ Peano Axioms）的算法（Peano Axioms ）的一組公理，但添加了量詞。 Peano當時不知道Frege的工作。大約在同一時間，理查德·德基德（Richard Dedekind）表明，自然數是其誘導特性的獨特特徵。 Dedekind提出了不同的特徵，這缺乏Peano公理的形式邏輯特徵。但是，Dedekind的工作證明了Peano系統中無法訪問的理論，包括一組自然數（直至同構）的獨特性以及對後繼功能和數學誘導的加法和乘法的遞歸定義。
在19世紀中葉，歐幾里得公理的幾何形狀中的缺陷已知。除了由尼古拉·洛巴喬夫斯基（Nikolai Lobachevsky）於1826年建立的平行假設的獨立性外，數學家還發現，歐幾里得（Euclid）認為是理所當然的某些定理實際上並非從他的公理中證明。其中之一是一條線包含至少兩個點的定理，或者是同一半徑的圓，其中心被該半徑隔開必須相交。希爾伯特（Hilbert）開發了一套完整的公理，用於幾何形狀，並在帕施（Pasch）的先前作品建立基礎上。公理化幾何形狀的成功促使希爾伯特（Hilbert）尋求對其他數學領域（例如自然數和實際線路）的完整公理。這將被證明是20世紀上半葉研究的主要研究領域。
19世紀的真實分析理論取得了巨大進步，包括功能和傅立葉系列的融合理論。諸如Karl Weierstrass之類的數學家開始構建伸展直覺的功能，例如無處可不同的連續功能。以前的函數作為計算或平滑圖的概念不再足夠。 Weierstrass開始主張分析的算法，該分析試圖使用自然數的特性進行公理化分析。 Bolzano在1817年已經開發了極限和連續功能的現代（ε，δ） - 定義，但仍然相對未知。庫奇（Cauchy）在1821年就無限量定義了連續性（請參見Dours d'Analyze，第34頁）。 1858年，Dedekind根據Dedekind削減理性數字提出了對實際數字的定義，這是當代文本中仍使用的定義。
喬治·坎托（Georg Cantor）開發了無限集理論的基本概念。他的早期結果發展了基礎性理論，並證明了真實和自然數量具有不同的基礎性。在接下來的二十年中，Cantor在一系列出版物中提出了一種遞延數字的理論。在1891年，他發布了一個新的證明，證明了引入對角線參數的實數的不可實數，並使用此方法證明Cantor的定理沒有集合可以與其PowerSet具有相同的基數性。 Cantor認為每組都可以井井有條，但無法為此結果提供證據，這在1895年將其視為一個懸而未決的問題。
20世紀
在20世紀初期，研究的主要領域是理論和正式邏輯。非正式集合理論中悖論的發現導致一些人懷疑數學本身是否不一致，並尋找一致性的證據。
1900年，希爾伯特（Hilbert）在下個世紀佔據了23個問題的著名清單。其中的前兩個是解決連續性假設並分別證明基本算術的一致性。第十是產生一種可以決定整數上的多元多項式方程的方法。隨後解決這些問題的工作構成了數學邏輯的方向，解決希爾伯特的ientscheidungsproblem的努力也在1928年提出。這個問題要求採用一個程序，鑑於正式的數學陳述，該陳述是正確還是錯誤。
設定理論和悖論
恩斯特·澤梅洛（Ernst Zermelo）證明了每套可以很好地訂購的，這是喬治·坎托（Georg Cantor）無法獲得的結果。為了獲得證明，Zermelo介紹了選擇的公理，該公理在數學家和集合理論的先驅中引起了激烈的辯論和研究。對這種方法的直接批評使Zermelo發布了他的結果的第二次闡述，直接解決了對他的證據的批評。本文導致在數學社區中普遍接受選擇的公理。
幼稚集理論中最近發現的悖論加強了對選擇公理的懷疑。 Cesare Burali-Forti是第一個陳述悖論的人： Burali-Forti悖論表明，所有序數的收集都無法形成一組。此後不久，伯特蘭·羅素（Bertrand Russell）在1901年發現了羅素的悖論，朱爾斯·理查德（Jules Richard）發現了理查德（Richard）的悖論。
Zermelo為集合理論提供了第一組公理。這些公理以及亞伯拉罕·弗拉克爾（Abraham Fraenkel ）提出的替代的其他公理現在稱為zermelo – fraenkel set理論（ZF）。 Zermelo的公理納入了大小的限制原則，以避免羅素的悖論。
1910年，羅素（Russell）和阿爾弗雷德（Alfred North Whitehead）的第一卷Mathematica發表了。這項開創性的工作在一個完全正式的類型理論框架中開發了功能和基數理論，羅素和懷特海德為避免悖論而發展。 Mathematica原理被認為是20世紀最具影響力的作品之一，儘管類型理論的框架並未被證明是數學基礎理論。
Fraenkel證明了選擇的公理不能從Zermelo的套裝理論的公理中證明。後來的保羅·科恩（Paul Cohen）的工作表明，不需要添加尿液元素，並且選擇的公理在ZF中是無法證實的。科恩的證明開發了強迫的方法，這現在是建立獨立性的重要工具。
符號邏輯
LeopoldLöwenheim和Thoralf Skolem獲得了Löwenheim-Skolem定理，該定理說一階邏輯無法控制無限結構的基礎性。 Skolem意識到該定理將適用於集合理論的一階形式化，這意味著任何此類形式化具有可數模型。這個違反直覺的事實被稱為Skolem的悖論。
庫爾特·戈德爾（KurtGödel）在他的博士學位論文中證明了完整的定理，該定理在一階邏輯中建立了語法和語義之間的對應關係。 Gödel使用完整的定理證明了緊湊的定理，證明了一階邏輯後果的限制性質。這些結果有助於將一階邏輯確立為數學家使用的主要邏輯。
1931年，戈德爾（Gödel）發表了關於原理數學和相關係統的正式命題的發表，這些命題證明了所有足夠強，有效的一階理論的不完整（以單詞的不同含義）。該結果被稱為Gödel的不完整定理，對數學基礎建立了嚴重的局限性，對希爾伯特的計劃造成了強烈打擊。它表明了在任何形式的算術理論中提供算術的一致性證明的不可能。但是，希爾伯特一段時間以來並沒有承認不完整定理的重要性。
Gödel的定理表明，如果系統一致，或任何較弱的系統中，則無法在系統本身中獲得任何足夠強，有效的公理系統的一致性證明。這留下了無法在其考慮的系統中形式化的一致性證明的可能性。 Gentzen使用有資格的系統以及跨越誘導原則證明了算術的一致性。 Gentzen的結果介紹了削減消除和證明理論的序列的思想，這成為證明理論的關鍵工具。戈德爾給出了不同的一致性證明，從而降低了經典算術在較高類型中直覺算術的一致性。
關於外行的符號邏輯的第一本教科書是由劉易斯·卡羅爾（Lewis Carroll）於1896年撰寫的。
其他分支的開始
阿爾弗雷德·塔斯基（Alfred Tarski）發展了模型理論的基礎知識。
從1935年開始，一群著名的數學家以化名尼古拉斯·布爾巴基（ Nicolas Bourbaki）合作，出版了一系列百科全書數學文本。這些文本以嚴峻而公理的風格寫成，強調了嚴格的演示和固定理論基礎。這些文本所創造的術語，例如生命，注射和陳述，以及所採用的文本的固定理論基礎，在整個數學過程中被廣泛採用。
對可計算性的研究被稱為遞歸理論或計算性理論，因為Gödel和Kleene的早期形式化依賴於功能的遞歸定義。當這些定義顯示等於圖靈（Turing）涉及圖靈機的形式化時，很明顯，已經發現了一個新概念（可計算功能），並且該定義足夠強大，足以承認眾多獨立的特徵。戈德爾在1931年關於不完整定理的工作中缺乏嚴格的有效正式系統的概念。他立即意識到，可計算性的新定義可以用於此目的，使他能夠說明普遍性的不完整定理，而原始論文中只能暗示。
斯蒂芬·科爾·克萊恩（Stephen Cole Kleene）和埃米爾·萊昂（Emil Leon Post）在1940年代獲得了許多遞歸理論的結果。克萊恩（Kleene）介紹了相對可計算性的概念，圖靈（Turing）和算術層次結構介紹了。 Kleene後來概括性遞歸理論到高階功能。克萊恩（Kleene）和喬治·克雷塞爾（Georg Kreisel）研究了直覺數學的形式版本，尤其是在證明理論的背景下。
形式邏輯系統
數學邏輯以此為核心，涉及使用形式邏輯系統表達的數學概念。儘管它們在許多細節上有所不同，但它們具有僅考慮固定形式語言表達式的共同屬性。命題邏輯和一階邏輯的系統是當今研究最廣泛的，因為它們適用於數學基礎，並且由於其理想的證明理論特性。還研究了更強的經典邏輯，例如二階邏輯或無限邏輯，以及非古典邏輯（例如直覺邏輯） 。
一階邏輯
一階邏輯是一種特定的正式邏輯系統。它的語法僅涉及有限表達式和良好的公式，而其語義的特徵是所有量詞限制對話語的固定領域。
正式邏輯的早期結果確定了一階邏輯的局限性。 Löwenheim– Skolem定理（1919）表明，如果一組可數的一階語言中的一組句子具有無限模型，那麼它至少具有每個無限基數的模型。這表明，一組一階公理不可能表徵自然數，實數或任何其他無限結構，直到同構。由於早期基礎研究的目的是為數學的所有部分產生公理理論，因此這種局限性尤為明顯。
Gödel的完整性定理確定了一階邏輯中邏輯後果的語義和句法定義之間的等效性。它表明，如果在滿足特定公理集的每個模型中，特定的句子是正確的，則必須從公理中扣除句子。緊湊型定理首先在戈德爾的完整性定理證明中是一種引理，而且邏輯學家花了很多年才掌握其意義，並開始定期應用它。它說，只有當每個有限子集都有一個模型，或者換句話說，一組不一致的公式必須具有有限的子集時，一組句子具有模型。完整性和緊湊性定理允許對一階邏輯和模型理論的發展進行複雜的邏輯後果分析，它們是數學中一階邏輯突出的關鍵原因。
Gödel的不完整定理對一階公理化建立了額外的限制。第一個不完整定理指出，對於能夠解釋算術的任何一致，有效地給出的邏輯系統（以下定義），存在一個真實的陳述（從某種意義上說，它適用於自然數字），但在該邏輯中卻無法證明系統（並且確實在某些可能與邏輯系統一致的非標準模型中可能失敗了）。例如，在每個能夠表達Peano Axioms的邏輯系統中，Gödel句子都具有自然數量，但無法證明。
如果可以在系統語言中確定任何公式，公式是否為公理，並且可以表達Peano Axioms的邏輯系統可以有效地給出，則可以有效地給出。當應用於一階邏輯時，第一個不完整的定理意味著任何足夠強，一致，有效的一階理論的模型都不是基本等效的，比löwenheim-Skolem定理建立的模型更強。第二個不完整定理指出，沒有足夠的強，一致，有效的公理系統可以證明其自身的一致性，這已被解釋為表明無法達到希爾伯特的計劃。
其他古典邏輯
除了一階邏輯外，還研究了許多邏輯。其中包括無限邏輯，允許公式提供無限量的信息和高階邏輯，這些信息直接在其語義中包括集合理論的一部分。
研究最精心的無限邏輯是。在此邏輯中，量詞只能像一階邏輯一樣嵌套到有限的深度上，但是公式可能具有有限的或次數無限的連接及其內部分離。因此，例如，可以說一個對像是使用這樣的公式
高階邏輯不僅允許量化話語領域的元素，還允許話語領域的子集，此類子集的集合和其他較高類型的對象進行量化。語義是定義的，因此，量詞範圍在適當類型的所有對像上，而不是為每個高型量化符具有單獨的域。在開發一階邏輯之前所研究的邏輯，例如弗雷格的邏輯，具有類似的集合理論方面。儘管高階邏輯具有更大的表現力，因此可以對自然數等結構進行完整的公理化，但它們不滿足一階邏輯的完整性和緊湊性定理的類似物，因此對證明理論分析的較低程度不足。
另一種類型的邏輯是允許歸納定義的固定點邏輯S，就像一個為原始遞歸函數寫作一樣。
一個人可以正式定義一階邏輯的擴展- 一個概念涵蓋了本節中的所有邏輯，因為它們以某些基本方式的行為像一階邏輯一樣，但並不包含所有邏輯，例如，它並不包含直覺主義的，模態或模糊邏輯。
Lindström的定理意味著，一階邏輯的唯一擴展使緊湊型定理和向下的Löwenheim-Skolem定理是一階邏輯。
非古典和模態邏輯
模態邏輯包括其他模態運算符，例如操作員，該操作員指出特定公式不僅是正確的，而且必然是正確的。儘管模態邏輯並不經常用於公理化數學，但它已被用來研究一階可預訂性和設定理論強迫的特性。
直覺邏輯是通過Heyting研究Brouwer的直覺計劃而開發的，Brouwer本人避免了形式化。直覺邏輯專門不包括排除中間的定律，該定律指出，每個句子都是真實的，或者其否定是真實的。克萊恩（Kleene）用直覺邏輯的證據理論的工作表明，可以從直覺的證據中恢復建設性信息。例如，直覺算術中的任何可證明的總功能都是可計算的。在諸如Peano算術之類的古典理論中，這是不正確的。
代數邏輯
代數邏輯使用抽象代數的方法研究形式邏輯的語義。一個基本的例子是使用布爾代數代表經典命題邏輯中的真實價值，以及使用Heyting代數代表直覺命題邏輯中的真實價值。使用更複雜的代數結構（例如圓柱代數）研究了更強的邏輯，例如一階邏輯和高階邏輯。
集理論
集合理論是集合的研究，它們是對象的抽象集合。在建立正式的集合理論的正式公理化之前，Cantor非正式地制定了許多基本概念，例如序數和基本數字。由於Zermelo而引起的第一個這樣的公理化略微擴展為Zermelo -Fraenkel Set理論（ZF），該理論（ZF）現在是數學中最廣泛使用的基礎理論。
已經提出了設定理論的其他形式化，包括von Neumann -Bernays -GödelSet理論（NBG）， Morse -Kelley Set理論（MK）和新基金會（NF）。其中，ZF，NBG和MK在描述集合的累積層次結構時相似。新基金會採用不同的方法。它允許對象諸如所有集合的集合以其集合存在公理的限制為代價。 Kripke – Platek集理論的系統與廣義遞歸理論密切相關。
集合理論中的兩個著名陳述是選擇的公理和連續假設。 Zermelo首先說明的選擇公理是由Fraenkel證明獨立於ZF的，但已被數學家廣泛接受。它指出，給定一組非空集的集合，有一個集合C完全包含集合中每個集合的一個元素。據說集合C從集合中的每個集合中“選擇”一個元素。儘管有些人認為做出這種選擇的能力被認為是顯而易見的，但由於該集合中的每個集合都是非空的，因此缺乏可以做出選擇的一般，具體規則，使其成為公理非構造性。 Stefan Banach和Alfred Tarski表明，可以使用的公理可以將實心球分解為有限數量的碎片，然後可以重新排列，而不會縮放，以製造兩個原始尺寸的實心球。該定理稱為Banach -Tarski悖論，是選擇公理的眾多違反直覺結果之一。
戴維·希爾伯特（David Hilbert）列為1900年的23個問題之一，最初提出的contor構假設是康托爾（Cantor）。選擇），通過開發連續假設必須擁有的可構造的集合理論的宇宙。 1963年，保羅·科恩（Paul Cohen）表明，連續假設不能從zermelo – fraenkel set理論的公理中證明。但是，這種獨立性結果並沒有完全解決希爾伯特的問題，因為新的理論的新公理可能可以解決該假設。儘管尚不清楚其重要性，但沿著這些線路的最新工作是由W. Hugh Woodin進行的。
集合理論中的當代研究包括大型樞機主教和決定性的研究。大型紅衣主教是具有特殊特性的主要特性，以至於在ZFC中無法證明這種基本主教的存在。通常研究的最小大型基數的存在，一種無法訪問的基數，已經意味著ZFC的一致性。儘管大型紅衣主教具有極高的基數，但它們的存在對真實線的結構有許多影響。確定性是指某些兩人遊戲的贏得策略的可能存在（據說遊戲是確定的）。這些策略的存在意味著真實線和其他波蘭空間的結構特性。
模型理論
模型理論研究了各種形式理論的模型。在這裡，理論是特定形式邏輯和簽名中的一組公式，而模型是一種對理論進行具體解釋的結構。模型理論與通用代數和代數幾何形狀密切相關，儘管模型理論的方法比這些領域更關注邏輯考慮。
特定理論的所有模型的集合稱為基礎類別。經典模型理論旨在確定在特定基本類中模型的屬性，或者確定某些類別的結構是否形成基本類別。
量化器消除的方法可用於證明特定理論的可定義集不能太複雜。塔斯基（Tarski）建立了對實際鎖定場的消除量詞，這一結果也表明了實數領域的理論。他還指出，他的方法同樣適用於代數封閉的任意特徵。由此發展的現代子場與O最低結構有關。
邁克爾·D·莫利（Michael D. Morley）證明的莫利（Morley ）的分類定理指出，如果具有可數語言的一階理論在某些不可數的基數中是絕對的，那麼這種基數的所有模型都是同構的，那麼它在所有無法達到的紅衣主教中都是絕對的。
連續假設的一個微不足道的後果是，一個遠小於連續性的完整理論，許多非同構可計數模型只能有很多。沃特的猜想以羅伯特·勞森·沃特（Robert Lawson Vaught）的名字命名，他說，即使是連續假設，這也是如此。已經建立了許多猜想的特殊案例。
遞歸理論
遞歸理論（也稱為可計算理論）研究了可計算函數和圖靈度的特性，將不可兼容的函數分為具有相同水平的不可兼容性的集合。遞歸理論還包括對廣義可計算性和確定性的研究。遞歸理論從1930年代的RózsaPéter ， Alonzo Church和Alan Turing的作品中發展出來，這在1940年代被Kleene和Post大大擴展。
古典遞歸理論的重點是從自然數到自然數的函數的可計算性。基本結果建立了使用圖靈機， λCliculus和其他系統的眾多獨立的，相等的特徵，建立了強大的規範可計算函數類別。更高級的結果涉及圖靈度的結構和遞歸列出的集合的晶格。
廣義遞歸理論將遞歸理論的思想擴展到不一定是有限的計算。它包括在高氧化理論和α-回歸理論等領域中對可計算性的研究。
遞歸理論的當代研究包括對算法隨機性，可計算模型理論和反向數學等應用的研究，以及純遞歸理論的新結果。
算法上無法解決的問題
遞歸理論的重要子領域研究算法不可分辨性。如果沒有可能的可計算算法將所有法律輸入的正確答案返回問題，則決策問題或功能問題在算法上是無法解決的。關於不可分辨性的第一個結果，於1936年由教堂和圖靈獨立獲得，表明ientscheidungsproblem在算法上是無法解決的。圖靈通過確定停止問題的無法解釋性來證明這一點，這一結果在遞歸理論和計算機科學中都具有極大的影響。
普通數學中有許多不可發現的問題的例子。 Pyotr Novikov在1955年無法解析，並於1959年獨立於W. Boone獨立證明了算法的問題。
希爾伯特（Hilbert）的第十個問題要求採用算法來確定具有整數係數的多元多項式方程是否在整數中具有解決方案。朱莉婭·羅賓遜，馬丁·戴維斯和希拉里·普特南取得了部分進展。 Yuri Matiyasevich在1970年證明了該問題的算法無法解釋性。
證明理論和建設性數學
證明理論是對各種邏輯扣除系統中形式證明的研究。這些證據表示為形式數學對象，通過數學技術促進了它們的分析。通常考慮使用幾種扣除系統，包括希爾伯特風格的扣除系統，自然扣除系統以及Extzen開發的序列微積分。
在數學邏輯的背景下，建設性數學的研究包括對直覺邏輯等非古典邏輯中系統的研究以及對謂語系統的研究。赫爾曼·韋伊爾（Hermann Weyl）的早期支持者是赫爾曼·韋伊爾（Hermann Weyl） ，他表明只有使用預性方法就可以開發大部分實際分析。
由於證明完全是有條理的，而在結構中的真理不是，因此在建設性數學中的工作很常見，可以強調可證明性。在古典（或非構造性）系統中的可易待性與直覺（或建設性）系統中的可拋態性之間的關係特別有趣。諸如Gödel -gentzen負翻譯之類的結果表明，可以將（或翻譯）經典邏輯嵌入直覺邏輯中，從而使有關直覺證明的某些屬性可以轉移回經典的證據。
證明理論的最新發展包括烏爾里希·科倫巴赫（ Ulrich Kohlenbach）對證明挖掘的研究以及邁克爾·拉特林（Michael Rathjen）的證明理論序列研究。
申請
“數學邏輯不僅成功地應用於數學及其基礎（ G. Frege ， B。Russell ， D。Hilbert ， P。Bernays ， H。Scholz ， R。Carnap ， S。Lesniewski ， T。Skolem ），而且還到物理學（R. Carnap，A。Dittrich，B。Russell， Ce Shannon ， Whitehead ， H。Reichenbach ，P。Fevrier），生物學（ JH Woodger ， A。Tarski ），心理學（ FB Fitch ， CG Hempel ） ，《法律與道德》（ K. Menger ，U。Klug，P。Oppenheim），經濟學（ J. Neumann ， O。Morgenstern ），用於實際問題（ Ec Berkeley ，E。Stamm），甚至是形而上學（J. [ Jan] Salamucha，H。Scholz， JM Bochenski ）。它在邏輯史上的應用已被證明非常富有成果（ J. Lukasiewicz ，H。Scholz， B。Mates ，A。Becker，A。Becker，E。Moody， E 。Moody ，J。Salamucha，k K 。 _ “也已對神學提出了申請（F. Drewnowski，J。Salamucha，I。Thomas）。”
與計算機科學的聯繫
計算機科學中計算理論的研究與數學邏輯中的可計算性研究密切相關。但是，重點有所不同。計算機科學家通常專注於具體的編程語言和可行的可計算性，而數學邏輯的研究人員通常將重點放在理論概念和非可測量性上。
編程語言的語義理論與模型理論以及程序驗證（特別是模型檢查）有關。證明與程序之間的咖哩 - 紐帶對應關係與證據理論有關，尤其是直覺邏輯。現在，將正式的微積分（例如Lambda微積分和組合邏輯）研究為理想化的編程語言。
計算機科學還通過開發自動檢查甚至發現證明的技術（例如自動定理證明和邏輯編程）來為數學做出貢獻。
描述性複雜性理論將邏輯與計算複雜性有關。 Fagin的定理（1974）在該領域的第一個重要結果確定， NP正是通過存在二階邏輯句子表達的一組語言。
數學基礎
在19世紀，數學家意識到了其領域的邏輯差距和不一致。結果表明，歐幾里得的公理用於幾個世紀以作為公理方法的一個例子，這是不完整的。由於發現了諸如WeierStrass諸如Weierstrass的無處可區分的連續功能之類的病理示例，因此無限量的使用以及功能的定義引起了質疑。
康托爾對任意無限集的研究也引起了批評。利奧波德·克羅內克（Leopold Kronecker）著名地說：“上帝製造了整數；其他一切都是人的作品”，認可重返數學中有限的混凝土物體。儘管克羅內克的論點是在20世紀由建構主義者提出的，但整個數學界拒絕了他們。戴維·希爾伯特（David Hilbert）主張對無限研究的研究表示：“沒有人將我們驅逐出坎托創造的天堂。”
數學家開始搜索可以用來形式化大部分數學的公理系統。除了從諸如函數之類的諸如函數之類的詞中消除歧義外，還希望這種公理化將允許一致性證明。在19世紀，證明一組公理的一致性的主要方法是為其提供模型。因此，例如，可以通過將點的指定點表示固定球和線上的點來表示一致，從而證明了非歐幾里得幾何形狀，以表示球體上的大圓圈。所得的結構是橢圓形的模型，除了平行的假設外，滿足了平面幾何形狀的公理。
隨著形式邏輯的發展，希爾伯特詢問是否可以通過分析系統中可能的證據結構來證明公理系統是一致的，並通過此分析表明，不可能證明是矛盾的。這個想法導致了對證明理論的研究。此外，希爾伯特（Hilbert）提出，分析應該完全具體，使用術語“限制”一詞來指他所允許但不能準確定義它們的方法。該項目被稱為希爾伯特（Hilbert）的計劃，受到戈德爾（Gödel）不完整定理的嚴重影響，該定理表明，無法使用這些理論中正式化的方法來確定正式理論的一致性。 Gentzen表明，有可能在以跨足誘導的公理增強的算術系統中產生算術的一致性證明，而他為此而發展的技術在證明理論中是開創性的。
數學基礎歷史上的第二個線程涉及非經典邏輯和建設性數學。對建設性數學的研究包括許多不同的程序，具有不同的建設性定義。在最包容的端，ZF集理論中不使用所選公理的證據被許多數學家稱為建設性。建構主義的更有限制的版本將自己限制在自然數，數量理論函數和一組自然數（可用於表示實數，促進數學分析研究）。一個普遍的想法是，必須在函數本身存在之前就必須知道計算函數值的具體方法。
在20世紀初期，盧森·埃格伯斯（Luitzen Egbertus）Jan Brouwer作為數學哲學的一部分創立了直覺主義。最初鮮為人知的這種哲學表明，為了使數學陳述忠於數學家，該人必須能夠直覺，不僅要相信其真理，而且還要理解其真理的原因。對真理的定義的結果是拒絕了被排除的中間法律，因為據布魯維爾說，有些陳述不能被認為是真實的，而他們的否定也不能被認為是真實的。布魯維爾的哲學具有影響力，是著名數學家發生痛苦爭議的原因。後來，克萊恩（Kleene）和克雷塞爾（Kreisel）將研究直覺邏輯的形式化版本（布勞維爾（Brouwer）拒絕形式化，並以非法規的自然語言介紹了他的作品）。隨著BHK解釋和Kripke模型的出現，直覺主義變得更容易與經典數學調和。