證明論的歷史發(fā)展梳理

摘 要：有關(guān)證明的思想由來已久，然而直到十九世紀(jì)末證明論才得以從古希臘的歐式幾何和三段論等簡單的思想中逐步豐富和完善，發(fā)展成為一門成熟的學(xué)科，并逐步從傳統(tǒng)數(shù)學(xué)領(lǐng)域逐步擴(kuò)展到計算機(jī)等其他學(xué)科。對證明論歷史發(fā)展脈絡(luò)的把我，對證明論的學(xué)習(xí)至關(guān)重要。

關(guān)鍵詞：證明論；證明；數(shù)學(xué)

證明論是數(shù)理邏輯的分支，主要以形式化方法研究數(shù)學(xué)證明，它是一種研究數(shù)學(xué)證明一般結(jié)構(gòu)的學(xué)科。對證明的研究并不是近現(xiàn)代才出現(xiàn)的，從古希臘開始，證明就被邏輯學(xué)家所關(guān)注，從亞里士多德的《后分析篇》中可以看到，古希臘人就已經(jīng)開始關(guān)注如何從假設(shè)的命題必然地得到結(jié)論。如歐氏幾何學(xué)，它是由公認(rèn)的五條幾何學(xué)知識描繪而成的公理系統(tǒng)，通過有限的公理必然地得出所有的歐式幾何的真命題。再如，亞里士多德三段論，邏輯學(xué)家將正確判斷推理的邏輯形式抽象出來，用若干規(guī)則加以規(guī)定并從這些規(guī)則出發(fā)判定一個推理是否有效。這些簡單的與證明有關(guān)的理論幾乎統(tǒng)治了邏輯學(xué)超過兩千年。

對一般數(shù)學(xué)證明的考察，必須對數(shù)學(xué)證明進(jìn)行符號化，歷史發(fā)展也證明了形式化方法對邏輯的發(fā)展產(chǎn)生了巨大推動作用。最早旗幟鮮明地主張符號化的是萊布尼茲，他提出將推理符號化，然后交付機(jī)器進(jìn)行計算，這被稱為演算推論器的思想。雖然萊布尼茲的研究重點并不是數(shù)學(xué)證明，但他的符號化的思想無疑是超前的，并對后世作為邏輯主義創(chuàng)始人之一的弗雷格產(chǎn)生了重要影響。1879年弗雷格《概念文字》一書出版，他用形式化方法創(chuàng)造了一種表意語言，消除了自然語言的歧義和含混，保證了推理過程的絕對嚴(yán)格性。除此之外，他將數(shù)學(xué)中的函數(shù)概念引入邏輯，建立了量詞理論，后來他用九條公理和四條變形規(guī)則構(gòu)造了歷史上第一個嚴(yán)格的邏輯演算系統(tǒng)，并認(rèn)為算數(shù)定理可以從邏輯系統(tǒng)中推導(dǎo)出來，甚至整個數(shù)學(xué)可以被劃歸到邏輯中來，后來羅素、懷特海和維特根斯坦等人都直接受益于弗雷格，弗雷格的思想對后來現(xiàn)代證明論的產(chǎn)生具有極大的影響。

十九世紀(jì)下半葉，康托爾的集合論已經(jīng)滲透到了數(shù)學(xué)的各個分支，受到了廣大數(shù)學(xué)家的接受，并且他們發(fā)現(xiàn)從自然數(shù)和康托爾集合論出發(fā)能夠構(gòu)筑整個數(shù)學(xué)大廈，因此集合論也被現(xiàn)代數(shù)學(xué)家奉為現(xiàn)代數(shù)學(xué)的基石。然而根據(jù)集合論，集合可以由任意元素（包括不屬于自己的元素）組成，如果集合A由不屬于A的元素構(gòu)成，那么顯然會陷入兩難境地，這就是著名的羅素悖論，它動搖了數(shù)學(xué)的基礎(chǔ)，并且引起了數(shù)學(xué)家和邏輯學(xué)家關(guān)于數(shù)學(xué)基礎(chǔ)問題的大討論。

“數(shù)學(xué)與邏輯結(jié)合，或者說數(shù)理邏輯發(fā)展的一個重要起點，就是數(shù)學(xué)求助于邏輯來證明自己的一致性。”[1]在數(shù)學(xué)基礎(chǔ)大討論的歷史背景下，大衛(wèi)·希爾伯特創(chuàng)立了證明論，并試圖證明整個數(shù)學(xué)的無矛盾性。歷史上對數(shù)學(xué)無矛盾性的討論僅限于采用化歸方法對非歐幾何的無矛盾性的證明，即在歐式幾何中構(gòu)造非歐幾何模型，用歐式幾何的無矛盾性證明非歐幾何的無矛盾性，這種做法將A理論的無矛盾性歸結(jié)為B理論的無矛盾性，但是B理論的無矛盾性又需要證明，顯然數(shù)學(xué)理論的無矛盾性必須給出絕對的證明，并且為了避免循環(huán)論證，不能采用數(shù)學(xué)中的理論來證明數(shù)學(xué)自身的無矛盾性，而必須使用數(shù)學(xué)理論之外的理論來證明，為此，希爾伯特提出了證明論的方法。這種方法將數(shù)學(xué)中的所有概念通過形式化的方法[2]由公理和推理規(guī)則確定下來。這樣，數(shù)學(xué)中的命題就變成了形式化的公式，命題之間的推演也就變成了形式化了的數(shù)學(xué)命題依據(jù)公理和推理規(guī)則進(jìn)行的變換。如果能夠證明這個公理系統(tǒng)不能得出兩個相互矛盾的公式，也就證明了數(shù)學(xué)的無矛盾性。希爾伯特的證明論思想一經(jīng)提出便備受關(guān)注，算術(shù)系統(tǒng)等一些簡單的數(shù)學(xué)理論的無矛盾性被證明，這無疑增強(qiáng)了人們對證明整個數(shù)學(xué)無矛盾性的信念。雖然歷史證明希爾伯特的理想是無法實現(xiàn)的，“但他所創(chuàng)立的證明論卻使得一門普通數(shù)學(xué)理論整體地作為一個確定的、可用數(shù)學(xué)方法來研究的對象”[3]。

1931年哥德爾不完全性定理的提出否定了希爾伯特從形式邏輯出發(fā)證明數(shù)學(xué)無矛盾性的構(gòu)想。哥德爾起初也是希爾伯特宏大構(gòu)想的追隨者，并試圖證明形式算術(shù)系統(tǒng)的無矛盾性，但發(fā)現(xiàn)這是不可能得證的，由此得到哥德爾不完全性定理。哥德爾不完全性定理的證明打破了希爾伯特的構(gòu)想，并且迫使希爾伯特及其追隨者修補(bǔ)其理論或轉(zhuǎn)向新的理論。

根岑將目光轉(zhuǎn)向數(shù)學(xué)家實際研究中使用的數(shù)學(xué)證明，并發(fā)現(xiàn)數(shù)學(xué)家的證明并不是基于類似于希爾伯特式的公理系統(tǒng)，而是基于一些假設(shè)的命題，從這些假設(shè)的命題得到一些結(jié)論，把假設(shè)的命題分解為它的組成部分，這個推理過程用“消去規(guī)則”來表示，相反，從結(jié)論的各個分解部分到結(jié)論自身的推理用“引入規(guī)則”來刻畫。基于此，根岑發(fā)明了相較于公理系統(tǒng)更貼近日常推理的證明系統(tǒng)，自然演繹系統(tǒng)。由于沒能證出古典自然演繹系統(tǒng)的正規(guī)化定理，根岑發(fā)明了矢列演算系統(tǒng)，該系統(tǒng)從形式上描繪了自然演繹系統(tǒng)中的可演繹關(guān)系，通過證明The Hauptsatz[4]（即cut消去定理）和證明所有的規(guī)則都具有子公式性質(zhì)，可以解決該系統(tǒng)中任意公式的判定性問題。

上世紀(jì)六十年代之后，證明論不在僅僅關(guān)注系統(tǒng)的無矛盾性問題，開始研究數(shù)學(xué)證明的一般結(jié)構(gòu)和性質(zhì)，證明的復(fù)雜性，數(shù)學(xué)中的不可判定性問題，并且逐步走出傳統(tǒng)數(shù)學(xué)，延伸向邏輯編程等計算機(jī)領(lǐng)域。

參考文獻(xiàn)

[1]陳慕澤. 正確理解哥德爾不完全性定理[J].湖南科技大學(xué)學(xué)報：社會科學(xué)版，2008，11（2）：27-30.

[2]Kreisel G. A survey of proof theory[J].Journal of symbolic Logic，1968：322.

[3]徐云從. 證明論及其發(fā)展[J].數(shù)學(xué)季刊：英文版，1988，（03）.

[4]Gentzen G. Investigations into logical deduction[J].American philosophical quarterly，1964：298.

作者簡介

黨學(xué)哲（1992-），男，河南洛陽人，西南大學(xué)政治與公共管理學(xué)院研究生，研究方向：現(xiàn)代邏輯。

（作者單位：西南大學(xué)政治與公共管理學(xué)院）