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

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

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

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

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

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

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

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

甘岑在第二次大戰(zhàn)行將結(jié)束時去世，他的結(jié)果代表當(dāng)時證明論的最高成就，希爾伯特和貝納斯的《數(shù)學(xué)基礎(chǔ)》第二卷中總結(jié)了他的工作，但是證明論遠(yuǎn)遠(yuǎn)未能完成它的最初目標(biāo)。戰(zhàn)后隨著模型論和遞歸論乃至六十年代以來公理集合論的發(fā)展，證明論一直進(jìn)展不大。

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

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

厄布朗及甘岑的結(jié)果雖然不可能完成希爾伯特計劃的最初目標(biāo)，但是由于其有限性、可構(gòu)造性的特點，現(xiàn)在已廣泛地應(yīng)用于機(jī)械化證明，成為這門學(xué)科的理論基礎(chǔ)。

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