證明論

　　數理邏輯的一個分支，以數學證明為研究物件的數學理論。

　　邏輯學中關於證明的研究由來已久。亞裡斯多德《工具論》一書中的《分析後篇》就是討論有關證明的問題的，並且他是以古希臘時期的數學中所用到的證明作為研究物件的。近代的證明理論開始於20世紀前期，是由德國數學傢D.希爾伯特創立的。希爾伯特有時將證明論與元數學（即數學基礎）視作同義語。希爾伯特學派所發展的證明論側重於公理系統的無矛盾性的研究，他們企圖用本身無可懷疑的方法（即希爾爾伯特等人所說的有窮方法，有時又稱作初等方法）來論證整個數學是無矛盾的。希爾伯特原來設想，從公理化算術開始，用有窮方法證明它的無矛盾性，然後證明數學分析以及集合論的無矛盾性等等。

　　1931年K.哥德爾證明瞭下列事實：在一個復雜到一定程度的公理系統中，如果這個系統是無矛盾的，則它是不完備的，而且它的矛盾性在這個系統中是無法證明的。這就證明瞭希爾伯特原來的方案是無法實現的。在這以後，有些邏輯學者打算降低原來的要求，采用可靠性比有窮方法低的方法來證明算術和數學分析的無矛盾性。G.根岑在1936年證明瞭算術的無矛盾性，60年代以來又有些人證明瞭數學分析的某些片斷的無矛盾性。

　　雖然希爾伯特學派關於證明論的研究專門註重數學系統無矛盾性的證明，但證明論本不應限於無矛盾性的證明的研究。G.克賴澤爾等人60年代以來，開始瞭關於證明的結構以及復雜度等問題的研究。1977年以來J.帕裡斯等人發現瞭算術中自然的不可判定的命題。後來有些人在從事這方面的研究，又獲得瞭一些重要的成果。

　　半個世紀以來，證明論的最重要的結果之一是哥德爾不完備性定理。根據這一定理可知，對復雜到一定程度的（這裡所說的“一定程度”是可以嚴格定義的）數學理論T而言，如果T是無矛盾的，則T是不完備的；也就是說，在這些理論中，總有一些命題，它們是真的，但不能由這些理論的公理推出。1977年以來，又發現在算術中存在著自然的不可判定的命題，也就是說，從算術的公理出發，既不能證明也不能否證的算術命題。

　　1931年時哥德爾就發現瞭算術中存在有不可判定的命題，後來文獻中稱之為哥德爾語句。這一語句G是說：“語句G是不可證的。”哥德爾語句是一個算術的命題，但不是自然的算術命題。算術中第一個自然的不可判定的命題是直到1977年才由帕裡斯等人發現的。這被認為是數理邏輯中一項重大成果。

　　克賴澤爾派的證明論以證明的結構和復雜度為研究對象。這方面的研究結果是與計算復雜性理論滲透交叉的；在計算機科學中，特別是在定理的機械化證明中可能有應用。

　　構造主義邏輯和構造性數學方面近年來也有不少成果。構造主義邏輯中最早提出的一種是荷蘭數學傢佈勞威爾在20世紀初提出的直覺主義邏輯。這是一種排中律在其中不成立，因而在其中不能用間接證明的邏輯（這裡所說的排中律不成立是指對無窮集而言；在直覺主義邏輯中，對有窮集而言，排中律還是成立的）。L.E.J.佈勞威爾提出這種邏輯是為瞭解決數學基礎方面的問題，也就是作為避免悖論的一種方案。實際上，構造傾向(即註重算法的傾向)一直是數學史上的一種重要傾向。20世紀40年代以來，由於電子計算機的發明和計算技術的發展，這一傾向更顯出其重要性。而且直覺主義邏輯已被發現與有些數學分支（如集合論中的力迫理論）有出人意料的聯系。

　　證明論的關於算術中的自然的不可判定的命題的研究正在引起越來越多的人註意。已有人猜測，數論中有些著名問題如黎曼猜測、費馬大定理和哥德巴赫猜想等都可能是算術中不可判定的命題。並且由於已知這些命題都是可以表示成∀nR(n)的形式的（這裡n是自然數，而R(n)是一個遞歸謂詞），而又知道，如果一個命題p可以表示成∀nR(n)的形式，而且p是在算術中不可判定的，則p不可能是假的，必然是真的。因此這一方向的研究更加令人註意。計算機科學中有些未解決的問題(如p=?Np)也有人猜測，是在算術中不可判定的。

　　

參考書目

　J.Barwise，ed.，Handbook of MatheMatical Logic，North-Holland，Amsterdam，1977.