證明論

證明論

proof theory

研究數學證明的數學理論。數理邏輯的分支學科。數學

中的證明一向是邏輯學家研究的對象，但證明論是數學家D.希爾伯特於20世紀初期建立的，目的是要證明公理系統的無矛盾性，希爾伯特提出一整套嚴格的方案，規定只能用有限長的證明，要無可辯駁地給出整個數學的無矛盾性。他打算先給出公理化的算術系統的無矛盾性，再證明數學分析，集合論的無矛盾性。但1931年，K.哥德爾證明：一個包含公理化的算術的系統中不能證明它自身的無矛盾性。這就是著名的哥德爾不完備性定理。這個結果使希爾伯特方案成為不可能。但1936年，G.根岑降低了希爾伯特的要求，允許使用無窮長的證明，證明了算術公理系統的無矛盾性。到1960年，數學分析的一些片斷的無矛盾性也被證明。20世紀60年代以後，證明論不再局限於無矛盾性的證明。數學證明中的結構，證明的複雜性，數學中不可判定問題都成為證明論的研究課題，1977年，J.帕里斯發現算術理論中的一個自然的而又是不可判定的命題，這是一個重大發現。它使算術中自然的不可判定命題的研究越來越受人注意。