希爾伯特方案

希爾伯特在20世紀20年代提出的用以證明數學的協調性的一個特定的方案。數學中在使用反證法時需要肯定數學的協調性；後來在發展非歐幾何的過程中，需要證明非歐幾何的協調性以便斷定平行公設的獨立性，即斷定它不能由幾何中別的公理推出，但非歐幾何只是數學的一個部門而且是新發展的部門，即使它的協調性受到懷疑，仍無礙於整個古典數學的協調性。

方案要求

希爾伯特方案首先要求把數學完全形式化，列出基本概念、公理以及基本推理規則，而且必須列舉詳盡無遺,使得數學中一切概念都可以從基本概念定義出來,各概念一切性質也都可以從公理與基本推理規則推出，因而不必再藉助於任何直覺、任何圖形。這樣一來，基本概念可以是任何滿足公理與基本推理規則的東西，從而可以把它們看作變元，進而把它們看作表示這些變元的符號,公理不外是由一些符號所組成的符號系列,基本推理規則不外是一些對這些符號系列加以變換的變形規則。如果在一理論中能夠推出兩個互相否定（互相矛盾）的符號系列來，這理論便叫做不協調的。這樣，只要能夠證明從作為數學公理的那些符號系列出發，並根據作為數學的基本推理規則的變形規則加以改變，而且無論如何也變換不出表示互相矛盾的兩個命題的符號系列，那么數學的協調就可以被證明。

方案探討

希爾伯特方案回答了當自然數以及邏輯概念都在探討考察之列、它們的協調性都有待審查時，能用什麼去探討、研究的問題。它認為，符號系列是具體的有限的東西，由推理規則所反映的變換是對具體的符號進行的變換，所以也是具體的有限的動作，是只對具體的有限的東西所進行的具體的有限的動作。這樣便可以限於有窮主義，而有窮主義的結果是隨時可以被驗證的，因此其結果的協調性是無容置疑的。

論證簡述

希爾伯特方案中的有窮主義論證與數學中一般推理過程的最大不同，在於對待全稱量詞‘‘所有的 ’’以及存在量詞‘‘有的 ’’的論證上。片 ( )指‘‘所有的 使得A( )成立’’，但一般說來， ‘‘所有的 ’’並不能都拿來一一驗證,看它是不是使A( )成立。到底根據什麼斷定片 ( )為真’’？辦法是,取一個變元 它既不被假定有任何性質，也不被假定有任何特殊結構，只是一般的 。如果對於這個變元 而證明了A( ),那么就可以斷定片 ( )。不過有窮主義對通常的論證，如對‘‘找不出使A( )成假的 ，所以片 ( )’’這類用反證法立論的論證是不承認的。有窮主義也不承認這樣一種論證， ‘‘反設每個 》使得A( )為假,（推導下去）將導致矛盾，故不可能每個 》非A( )，於是至少有一個 A( )為真’’。因為在有窮主義看來,‘‘從片A( )可導致矛盾’’這個事實，並沒有給出具體的使為的 ，也沒有給出尋找這個 的方法。根據有窮主義的要求證明掣 ( )，是給出一個使得A( )成立的 。如果這個難馬上給出，至少也要給出一個尋找這個 的辦法如果真的能夠用有窮主義的論證證明形式化的數學是協調的，那么形式化數學的協調性便得以建立。因為有窮主義論證本身的協調性應該是沒有疑問的，所以數學協調性的直接證明也可以說沒有疑問的。

方案延伸

希爾伯特方案提出後不久，德國數學家W.阿克曼於1924年證明，如對數學歸納法稍作限制則自然數論是協調的。但K.哥德爾1931年卻證明，只用可以表示於內容相當豐富的數學系統S之內的理論，絕不能證明系統S的協調性。而希爾伯特方案要求的有窮主義論證是可以表述於自然數論之內的。這就表明，純粹使用有窮主義論證決不能證明自然數論的協調性，更不能證明整個數學的協調性。於是，希爾伯特方案最終宣告破產。後來的研究逐漸把有窮主義的要求放寬，繼續探討各理論系統的協調性以及和證明有關的各種性質，從而形成了證明論。