希爾伯特方案
正文
D.希爾伯特在20世紀20年代提出的用以證明數學的協調性的一個特定的方案。數學中在使用反證法時需要肯定數學的協調性;後來在發展非歐幾何的過程中,需要證明非歐幾何的協調性以便斷定平行公設的獨立性，即斷定它不能由幾何中別的公理推出，但非歐幾何只是數學的一個部門而且是新發展的部門，即使它的協調性受到懷疑，仍無礙於整個古典數學的協調性。等到人們依次地把非歐幾何的協調性化歸於歐幾里得幾何的協調性，再化歸於實數論、自然數論，最後化歸於集合論的協調性，而同時又發現素樸集合論有矛盾、不協調以後，數學的協調性問題就成為一個重大問題了。嚴格公理集合論雖然可以排除已被發現的悖論，但還不能保證數學理論里不再出現邏輯矛盾。要想徹底解決數學的協調性問題，用化歸方法是不夠的，因為這只能得到相對的協調性，而集合論的協調性不能再化歸於其他理論。同時希爾伯特認為在物理世界裡也找不到集合論里各種超窮集合的模型，因此，只有從事直接協調性證明才能得出真正的協調性。於是，他便提出其有名的方案。希爾伯特方案首先要求把數學完全形式化，列出基本概念、公理以及基本推理規則，而且必須列舉詳盡無遺,使得數學中一切概念都可以從基本概念定義出來,各概念一切性質也都可以從公理與基本推理規則推出，因而不必再藉助於任何直覺、任何圖形。這樣一來，基本概念可以是任何滿足公理與基本推理規則的東西，從而可以把它們看作變元，進而把它們看作表示這些變元的符號,公理不外是由一些符號所組成的符號系列,基本推理規則不外是一些對這些符號系列加以變換的變形規則。如果在一理論中能夠推出兩個互相否定（互相矛盾）的符號系列來，這理論便叫做不協調的。這樣，只要能夠證明從作為數學公理的那些符號系列出發，並根據作為數學的基本推理規則的變形規則加以改變，而且無論如何也變換不出表示互相矛盾的兩個命題的符號系列，那末數學的協調就可以被證明。
希爾伯特方案回答了當自然數以及邏輯概念都在探討考察之列、它們的協調性都有待審查時，能用什麼去探討、研究的問題。它認為，符號系列是具體的有限的東西，由推理規則所反映的變換是對具體的符號進行的變換，所以也是具體的有限的動作，是只對具體的有限的東西所進行的具體的有限的動作。這樣便可以限於有窮主義，而有窮主義的結果是隨時可以被驗證的，因此其結果的協調性是無容置疑的。希爾伯特方案中的有窮主義論證與數學中一般推理過程的最大不同，在於對待全稱量詞“所有的x”以及存在量詞“有的x”的論證上。凬xA(x) 指“所有的x均使得A(x)成立”，但一般說來，“所有的x”並不能都拿來一一驗證,看它是不是使A(x)成立。到底根據什麼斷定凬xA(x)為真”？辦法是,取一個變元x,它既不被假定有任何性質，也不被假定有任何特殊結構，只是一般的x。如果對於這個變元x而證明了A(x),那末就可以斷定凬xA(x)。不過有窮主義對通常的論證，如對“找不出使A(x)成假的x，所以凬xA(x)”這類用反證法立論的論證是不承認的。有窮主義也不承認這樣一種論證，“反設每個x都使得A(x)為假,（推導下去）將導致矛盾，故不可能每個 x都非A(x)，於是至少有一個x使A(x)為真”。因為在有窮主義看來,“從凬xA(x)可導致矛盾”這個事實，並沒有給出具體的使為真的x，也沒有給出尋找這個x的方法。根據有窮主義的要求證明ヨxA(x)，是給出一個使得A(x)成立的x。如果這個x很難馬上給出，至少也要給出一個尋找這個x的辦法。如果真的能夠用有窮主義的論證證明形式化的數學是協調的，那末形式化數學的協調性便得以建立。因為有窮主義論證本身的協調性應該是沒有疑問的，所以數學協調性的直接證明也可以說沒有疑問的。
希爾伯特方案提出後不久，德國數學家W.阿克曼於1924年證明，如對數學歸納法稍作限制則自然數論是協調的。但K.哥德爾1931年卻證明，只用可以表示於內容相當豐富的數學系統S之內的理論，絕不能證明系統S的協調性。而希爾伯特方案要求的有窮主義論證是可以表述於自然數論之內的。這就表明，純粹使用有窮主義論證決不能證明自然數論的協調性，更不能證明整個數學的協調性。於是，希爾伯特方案最終宣告破產。後來的研究逐漸把有窮主義的要求放寬，繼續探討各理論系統的協調性以及和證明有關的各種性質，從而形成了證明論。
