苗族音樂

[拼音]：zhengminglun

[英文]：proof theory

數理邏輯的一個分支。它最初的目的是想證明數學的協調性，後來逐漸推廣到探求一般的公理系統的協調性。數學中使用反證法時需要肯定數學的協調性。在證明歐幾里得平行公設不能由別的公理推出時，也就是證明平行公設的獨立性時，又需要肯定使用新公設的非歐幾何的協調性，這便要求人們對數學的一部分（非歐幾何）的協調性作出嚴格的探討與證明。這種協調性的證明起初是靠化歸方法獲得的，即把非歐幾何的協調性化歸於歐幾里得幾何的協調性，然後依次化歸於實數論的協調性、自然數論的協調性，最後化歸於集合論的協調性。這是所謂相對協調性的證明。但是，集合論的協調性比之自然數論的協調性更不明顯，而且由於集合論悖論的發現，表明了未經改造的素樸集合論也是不協調的。經過改造的嚴格公理化的集合論產生以後，雖然排除了已被發現的悖論，但還不能保證數學理論裡不再出現邏輯矛盾，而集合論的協調性問題又不能化歸於其他數學理論。同時，D.希爾伯特認為在物理世界裡是找不到集合論的模型的。為了解決這個協調性問題，他於20世紀20年代提出了著名的“希爾伯特方案”。由這個方案產生了證明論。

證明論的根本做法是：把所探討的理論系統（例如數學）完全形式化，作為研究物件，叫做物件理論。物件理論被當作沒有內容的，只是根據一定語法規則由一些被稱做字母的基本符號組成的一些符號序列，這些符號序列根據一定變形規則而變化。如果能夠匯出 A和塡A兩個符號序列，指經過解釋後表示互相矛盾的兩個命題，則說這理論是不協調的；如果無論怎樣變形都不能得出這種符號序列，便說這理論是協調的。證明論的目的是探討怎樣的理論是協調的，怎樣的理論是不協調的，尤其是要證明，數學作為物件理論是協調的。證明論還涉及到一種被稱為元理論的理論，它必須是有內容、有意義的。這樣，證明論就有了 3個理論，即：

（1）希望證明其協調性的那個沒有形式化的直觀的理論。它是有內容有意義的。它不是物件理論，只是物件理論的來源。

（2）物件理論。它是通過把所研究的理論完全形式化而得到的。它被當作沒有內容意義的，只是對一些符號序列作各式各樣的變形，是研究的物件。

（3）元理論。它是有內容意義的，是用來研究物件理論的，它應儘可能地簡單明瞭，使得人們至少相信它是協調的。元理論可以是第一個理論的一部分，但也可以是另外一個理論。在希爾伯特方案中，為了保證和說明元理論的協調性，至少是使人們相信元理論是協調的，對元理論作了非常嚴格的要求，要求它滿足有窮主義性，從而可以在直覺上保證它是協調的。但是滿足有窮主義性的理論，幾乎全可以表示在任何一個想證明其為協調的那些內容較為豐富的理論之內。K.哥德爾在1931年證明，要想證明一個理論S的協調性，使用能夠表示於S之內的理論是不行的，必須使用不能全部表示於 S之內的理論。這就是說，要證明S的協調性，元理論絕不能表示於S之內。

證明論是數理邏輯發展的產物，又是數理邏輯進一步發展的動力。如果沒有數理邏輯的發展，如果未能把數學的各個部門乃至一般理論系統形式化、公理化，就得不到物件理論，也就無法從事證明論的研究。證明論建立以來，已獲得一些重要的結果。1924年，德國數學家W.阿克曼證明：如對數學歸納法作一些限制，自然數論是協調的。

在哥德爾1931年的不完全性定理之後，對元理論的要求也放寬了。1936年德國數學家G.根岑證明引用超窮歸納法可以證明自然數論是協調的。這是證明論的最好結果。後來的研究又證明，加以相當限制的實數理論，即加以相當限制的數學分析是協調的。在這些證明中，只有阿克曼在1924年的證明是嚴格遵守有窮主義的，別的證明由於在哥德爾結果之後，已不限於有窮主義。因為根據哥德爾的結果，滿足有窮主義的元理論是相當弱的。但放寬的標準頗不相同，有的儘量少放寬，力圖靠近有窮主義；有的則大量放寬，得到了一些結果。