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

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

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

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

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

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

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

參考文獻(xiàn)

[1]陳慕澤. 正確理解哥德爾不完全性定理[J].湖南科技大學(xué)學(xué)報(bào)：社會(huì)科學(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.

作者簡(jiǎn)介

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

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