1930年以后，數學邏輯開始成為一個專門學科，得到了蓬勃發展。哥德爾的兩個定理證明之后，希爾伯特的有限主義綱領行不通，證明論出現新的情況，主要有兩方面：通過放寬有限主義的限制來證明算術無矛盾性以及把證明形式化、標準化，這些主要是在三十年代完成。同時哥德爾引進遞歸函數，發展成遞歸論的新分支，開始研究判定問題。而哥德爾本人轉向公理集合論的研究，從此出現公理集合論的黃金時代。五十年代模型論應運而生，它與數學有著密切聯系，并逐步產生積極的作用。

　　1、證明論

　　證明論又稱元數學，它研究數學的最基本活動—證明的合理性問題。研究這類數學基礎的問題原來一直是哲學家的事，后來才成為數學家的事。這個轉變發生在1893年弗雷格發表《算術基礎規則》之時，后來希爾伯特和他的許多合作者使這種思想發展成一門學科—元數學，目的是用數學方法來研究整個數學理論。

　　要使數學理論成為一個合適的研究對象，就必須使之形式化。自從希爾伯特和阿克曼所著《理論邏輯綱要》第一版在1928年出版以來，在實踐中用得最多的是具有等式的一階謂詞演算(以及高階謂詞演算)。許多理論可以用一階理論來表述，它比較簡單方便，具有多種形式。

　　從基礎的觀點來看，有兩個理論最為重要，因而研究也最多。這兩個理論就是形式化的皮亞諾算術理論與形式化的集合論。因為大多數觀代數學理論都可以在這兩個理論范圍內發展，所以這兩個理論的合理性如果得到證實，也就是向數學的可靠性邁進了一大步。“希爾伯特計劃”無非就是要找到一個有限的證明步驟來證明算術的無矛盾性。

　　這里“有限”的意義是由法國年輕數學家厄布朗明確提出的，他認為下列條件必須滿足：必須只討論確定的有限數目的對象及函數；這些對象及函數要能確定它們的真值產生協調一致的計算結果；一個對象如不指出如何構造它就不能肯定其存在；必須永遠不考慮一個無窮集體中所有對象的集合；一個定理對于一組對象都成立的意思是，對于每個特殊的對象，可以重復所講的普遍論證，而這普遍論證只能看成是結果特殊論證的原型。

　　數學理論的無矛盾性有了這種有限的、可構造性的論證之后，任何人都可以放心了。希爾伯特計劃提出后，幾組數學家分別為實現它而努力：一組是希爾伯特及貝耐斯，以及阿克曼關于把數學理論形式化的研究，一組是馮·諾依曼關于算術無矛盾性的初步研究及哥德爾的不完全性定理以及甘岑的最后解決；還有一組是厄布朗及甘岑關于證明的標準形式等的研究。

　　厄布朗是法國天才的青年數學家，1931年8月在登阿爾卑斯山時遇難，年僅23歲。他對代數數論尤其是數理邏輯進行過重要的研究工作，1929年他在博士論文《證明論研究》中提出他的基本定理。從某種意義上來講，這個定理是想把謂詞演算歸結為命題演算。由于前一理論是不可判定的，而后一理論是可判定的，因此這種歸結不可能是完全的。

　　但是，由于厄布朗局限于希爾伯特有限主義立場，他應用的證明方法比較繞彎子。而且在1963年發現，他的證明中有漏洞，他的錯誤很快就得到了彌補。厄布朗定理可以便我們在證明中擺脫三段論法。他的許多結果，后來也為甘岑獨立地得出。

　　甘岑的自然演繹系統是把數學中的證明加以形式化的結果。他由此得出所謂“主定理”，即任何純粹邏輯的證明，都可以表示成為某種正規形式，雖然正規形式不一定是唯一的。為了證明這個主定理，他又引進了所謂的式列(Sequenz)演算。

　　在普通的數學證明中，最常用則是三段論法，即如果A→B，且若A成立，則B成立。其實這就是甘岑推論圖中的“斷”。但是甘岑的主定理就是從任何證明圖中可以消除掉所有的“斷”。也就是：如果在一個證明中用到三段論法，那么定理表明，它也可以化成為不用三段論法的證明，也得到同樣的結論。

　　這個定理乍一看來似乎不可理解，其實正如甘岑所說，一個證明圖中有三段論法實際上是“繞了彎子”，而不用三段論法是走直路。這種沒有三段論法的證明圖稱為“正規形式”，利用這沒有三段論法的證明圖稱為“正規形式”。利用這個主定理很容易得出許多重要結果，其中之一就是極為簡單地證明“一階謂詞演算是無矛盾的”，而且能夠推出許多無矛盾性的結果。后來還可以用來證明哥德爾的完全性及不完全性定理，當然，最重要的事還是要證明算術的無矛盾性。

　　希爾伯特引進證明論的目標是證明整個數學的無矛盾性，其中最重要的是集合論的無矛盾性(至少ZF系統無矛盾)、數學分析的無矛盾性，最基本的當然是算術的無矛盾性。哥德爾的不完全性定理說明，用有限的辦法這個目標是達不到的。由于哥德爾不完全定理的沖擊，希爾伯特計劃需要修改。

　　有限主義行不通就要用非有限的超窮步驟。1935年，甘岑用超窮歸納法證明自然數算術形式系統的無矛盾性。其后幾年，他和其他人又給出了其他的證明。這種放寬了的希爾伯特計劃在第二次世界大戰之后發展成為證明論的分支，這些證明也推廣到分支類型論及其他理論。

　　甘岑在第二次大戰行將結束時去世，他的結果代表當時證明論的最高成就，希爾伯特和貝納斯的《數學基礎》第二卷中總結了他的工作，但是證明論遠遠未能完成它的最初目標。戰后隨著模型論和遞歸論乃至六十年代以來公理集合論的發展，證明論一直進展不大。

　　五十年代中，日本數學家竹內外史等人開始對于實數理論(或數學分析)的無矛盾性進行探索。因為實數一開始就同有理數的無窮集和有關，描述它的語言用一階謂詞演算就不夠了，所以第一步就要先把甘岑的工作推廣到高階謂詞演算中去。

　　1967年，日本年輕數學家高橋元男用非構造的方法證明，單純類型論中也可以消去三段論法。由此可以推出數學分析子系統的無矛盾性。但是，由于證明不是構造的，數學分析的無矛盾性至今仍然有待解決。

　　厄布朗及甘岑的結果雖然不可能完成希爾伯特計劃的最初目標，但是由于其有限性、可構造性的特點，現在已廣泛地應用于機械化證明，成為這門學科的理論基礎。

　　證明論的方法對于數理邏輯本身有很大的推動，特別是得出新的不可判定命題。最近，英國年輕數學家巴黎斯等人有了一項驚人的發現。他們發現了一個在皮亞諾算術中既不能證明也不能否證的純粹組合問題，這不僅給哥德爾不完全性定理一個具體的實例，而且使人懷疑要解決許多至今尚未解決的數論難題可能都是白費力氣。這無疑開辟了證明論一個完全新的方向。

　　2、遞歸論

　　遞歸論討論的是從形式上刻劃一個運算或一個進程的“能行”性這種直觀的觀念，也就是從原則上講，它們能機械地進行而產生一個確定的結果。“能行”的這個概念含有可具體實現的、有效的、有實效的等等意思。法國數學家保萊爾首先在1898年他的函數論教科書中引進了這個詞，他把數學的對象局限于能行的對象，這種主張實際上就是“法國經驗主義”。因為函數論主要討論集合、函數、積分等等，從這種觀點產生出描述集合論、拜爾函數等概念。

　　遞歸論中所討論的函數是比較簡單的。它討論有效可計算的函數，也就是遞歸函數。遞歸函數在歷史上曾從不同角度提出來，后來證明它們都是等價的。

　　1931年秋天，丘奇在普林斯頓開了一門邏輯課，克林和羅塞爾當時作為學生記了筆記。丘奇在講課中引進了他的系統，并且在其中定義自然數。這就很自然引起一個問題，在丘奇系統中如何發展一個自然數理論。于是克林開始進行研究，結果克林和丘奇得到一類可計算的函數，他們稱之為A可定義函數。

　　1934年春天，哥德爾在普林斯頓做了一系列講演(克林和羅塞爾記了筆記)。在講演中，哥德爾引進了另外一套可以精確定義的可計算函數類，他稱為一般遞歸函數。據他講，他是受了厄布朗的啟發得到的。

　　這時自然出現了一個問題。一般遞歸函數類是否包括所有能行可計算的函數，它是否與克林與丘奇研究的A可定義函數類重合。1934年春末，丘奇和哥德爾討論一般遞歸函數問題，結果丘奇明確提出他的“論點”，所有直覺上可看成能行可計算函數都是λ可定義函數，于是丘奇花了好幾個月反復思考。當時克林表示懷疑，他認為這論點不太可能是對的，他想如果從A可定義函數類用對角化方法可以得出另外一個能行可計算函數，那么它就不是A可定義的。但他又想到這事行不通。不久之后，丘奇和克林在1936年分別發表論文，證明A可定義函數類正好就是一般遞歸函數類。有了這個有力的證據，丘奇于是公開發表他的“論點”。

　　也是在1936年，英國年輕數學家圖林發表了另外一篇重要文章，這標志著所謂圖林機的產生。在這篇文章中，圖林也定義了一類可計算函數，也就是用圖林機可以計算的函數。同時，他也提出他的一個論點：“能行可計算的函數”與“用圖林機可計算的函數”是一回事。1937年圖林證明了用圖林機可計算的函數類與可定義函數類是一致的，當然，也就和一般遞歸函數類相重合。這樣一來，丘奇的論點與圖林的論點就是一回事。當時許多人對于丘奇的論點表示懷疑，由于圖林的思想表述得如此清楚，從而消除了許多人的疑慮，哥德爾就是其中一位。從這時起大家對于丘奇—圖林論點一般都抱支持的態度了。

　　與圖林同時，美國數學家波斯特也發表了一篇文章，類似于圖林的可計算函數，他的文章過于簡短，一直到1943年波斯特才發表了第四個表述，結果證明他的與別人的也都一樣。

　　遞歸的概念并不難理解，它就是由前面的結果可以遞推得到后面的結果。哥德爾等人引進的實際上是一般遞歸函數，一股遞歸函數都可以由原始遞歸函數算出來。

　　另一個復雜一些的概念稱為遞歸集合S，它的定義是存在一種能行的辦法來判斷任何正整數n是否屬于S。正數數集合是遞歸的當且僅當它與它在N中的補集都是遞歸可枚舉的。任何無窮遞歸可枚舉集都包含一個無窮遞歸集。但是，存在正整數的遞歸可枚舉集而不是遞歸集。

　　于是波斯特提出問題：是否存在兩個遞歸可按舉但是非遞歸的集合，使得第一個集合相對于第二個是遞歸的，但第二個相對于第一個卻不是遞歸的。一直到十二年后的1956年，蘇聯人穆其尼克及美國人弗里德伯格才獨立地肯定地解決了這個問題。

　　蘇聯數學家馬爾科夫在1947年發表《算法論》，首先明確提出算法的概念。但是它同以前定義的遞歸函數及可計算函數的計算過程都是等價的。這幾個定義表面上很不相同，并有著十分不同的邏輯出發點，卻全都證明是等價的。這件事看來決非巧合。它表明：所有這些定義都是同一個概念，而且這個概念是自然的、基本的、有用的。這就是“算法”概念的精確的數學定義。大家都接受了這個定義之后，判定問題從我們平時直觀的概念也上升為精確的數學概念，判定問題也成為一門數理邏輯的重要分支了。從這時起，判定問題有突飛猛進的發展。

　　判定問題有了精確的數學表述之后，立即在數學基礎乃至整個數學中產生了巨大的影響。因為這時一些不可判定命題的出現，標志著人們在數學歷史上第一次認識到：有一些問題是不可能找到算法解的。在過去，人們一直模模糊糊地覺得，任何一個精確表述的數學問題總可以通過有限步驟來判定它是對還是錯，是有解還是沒有解。找到不可判定問題再一次說明用有限過程對付無窮的局限性，它從另外一個角度反映了數學的內在固有矛盾。

　　怎樣得到這些結果的呢？丘奇的論點發表之后，不難看出存在不可計算的函數，也就是非一般遞歸的函數。因為所有可能不同的算法共有可數無窮多(粗淺來講，算法都是用有限多個字來描述的)，可是所有數論函數的集合卻是不可數的。

　　不過，頭一個明顯的不可判定的結果是1936年丘奇得到的。他首先得到與λ可定義性有關的不可判定結果。然后，他把這個結果應用到形式系統的判定問題上，特別他證明，形式化的一階數論N是不可判定的。也是在1936年，丘奇證明純粹的謂詞演算也是不可判定的。當時大家的反應是：這種不完全性的范圍到底有多廣？

　　甚至于象丘奇這樣的數學家，也想找到一條出路能避開哥德爾的結果。比如說，可以采用伺哥德爾所用的系統完全不同的其他的特殊系統。一旦算法的精確定義和丘奇論點出現之后，大家就認識到躲不過哥德爾不完全性定理的影響，可計算性和不完全性這兩個概念是緊密聯系在一起的。

　　實際上克林在1936年就證明了(作為丘奇論點的應用)：甚至在能夠能行地認出公理和證明的形式系統中，哥德爾的定理仍然成立。消去量詞方法對許多理論行不通。一般的判定問題是試圖找出一個能行的步驟，通過這個步驟可以決定什么東西具有某種指定的元數學特征。

　　在純粹邏輯演算的元理論中，有最明顯的一類判定問題：對于給定的演算和給定類的公式，求出一個步驟，能夠在有限多步內判定這類的任何特殊公式是否可以形式地推導出來。有些情形、問題已經得到肯定的解決，在另外一些情形，答案是否定的，可以證明不存在這樣一個步驟。這種否定的證明，特別對于數學理論，很大程度上依賴于遞歸論。

　　最早明確提出的數學判定問題是希爾伯特第十問題。他在1900年國際數學家大會上提出了著名的二十三個問題，其中第十個問題是：給定一個有任意多未知數的、系數為有理整數的丟番圖方程，設計一個步驟，通過它可以經有限步運算判定該方程是否有有理整數解。這個到1970年才被否定解決的問題不僅解決了一個重大問題，而且解決問題過程中所得到的工具和結果對數理邏輯和數學發展有著極大影響，比如表示素數的多項式，尤其與整個數理邏輯有關的是得出了一個更確切的哥德爾不完全性定理。

　　現在我們來看希爾伯特第十問題，為了清楚起見，我們考慮多項式方程，看看一般的多項式丟番圖方程的次數和未定元的數目是否可以降低。

　　1938年斯科蘭姆證明，任何丟番圖方程的次數可約化成次數小于等于4的方程；1974年馬蒂亞謝維奇和羅濱遜證明未定元的數目可約化成小于等于3。對于齊次方程，阿德勒在1971年證明，任何齊次方程可以能行地約化為二次齊次方程組，從而等價于一個四次齊次方程。對于一次方程早就有具體方法解丟番圖方程了。對于任意多未定元的二次方程，1972年西格爾也找到一個算法。四次方程不能判定，三次方程尚不知道。

　　解決丟番圖方程解是否存在的判定問題的方法是引進丟番圖集。我們把丟番圖方程的變元分成兩有一組解。每個丟番圖集合是遞歸可枚舉集。1970年，蘇聯大學生馬蒂亞謝維奇證明了每個遞歸可枚舉集也是丟番圖集合。這樣一來，由于存在不可判定的遞歸可枚舉集，所以存在一些特殊的丟番圖方程，使得對是否有解的判定問題不可解。當然對一般丟番圖方程的判定問題就更不可解了。

　　另一個判定問題是半群和群論中字的問題，半解問題是挪威數學家圖埃在1907年首先提出來的。問題是對于一個半群，如果給定它的有限多生成元和有限多關系，那么能否找到一個方法來判定任何一個特殊的字是否等于單位元素。1947年，波斯特否定地解決了這個問題。

　　群論中字的問題更為重要，它是在1911年由德恩首先研究的，一直到1955年才由蘇聯數學家諾維科夫否定解決。這些結果給數學家指明了新的方向：不要妄圖去解決一大類問題。不過對于更窄的一類的對象比如一類特殊的群，群的字問題是可解的。