不可勝數

用4523659424929個符號定義1

- 形式化的數學繁瑣冗長,卻是電腦進入數學推理的重要基石。

撰文/李國偉
2008-08

不可勝數

用4523659424929個符號定義1

- 形式化的數學繁瑣冗長,卻是電腦進入數學推理的重要基石。

撰文/李國偉
2008-08


在世界數學史裡,歐幾里得的《幾何原本》是達到嚴謹證明的第一個高峰。古希臘學者歷經不可公度量的困擾,以及辯者哲學詭論的攪局,逐漸發展出邏輯推理方法,因而得以有系統地組織幾何知識,在歐幾里得手中完成總結的工作。


這套西方學界奉為圭臬的公理化系統,影響的範圍遠超出數學領域。但是到了19世紀末葉,這座飽經風霜考驗的堡壘,終於出現了龜裂滲漏,涉及數學基礎的詭論紛至沓來。因此數學巨擘希爾伯特率先倡議形式主義(formalism),認為應該把平日訴諸直覺的數學論證,更加嚴明地形式化。也就是在限定範圍的原始符號、推論規則,以及基本公設的基礎上,逐步推導出數學家感興趣的命題,並且要保證這些形式系統不會發生內在矛盾。這種清理工作在小範圍的特定領域裡,確實可以取得相當成果。然而著名的哥德爾不完備定理,卻徹底破滅了把整體數學形式化的美夢,從而形式化只能在局部範圍裡進行才有意義。


其實形式化會帶來一種令人不悅的後遺症,那就是直覺中相當簡明的事物,形式化以後反而變得繁瑣冗長。這是因為數量不多的原始符號與基本公設意涵淺顯,想由此衍生出其他各式各樣的概念,幾乎無法迴避漫長的推導歷程。譬如羅素與懷海德的名著《數學原理》由初等邏輯出發,經過第一卷的第666頁至第二卷的第86頁,才證明了1+1=2。以這種龜速形式化數學,怪不得寫到第三卷就難以為繼了。


一種因應形式化過份瑣碎的方式,是把有用的數學領域半形式化。也就是在適度的篇幅裡盡量形式化,而那些未能完全形式化的概念,根據系統開展的方式,如有必要「原則上」也能夠完全達到形式化。


從半形式化到全形式化的過程中,同一個直覺數學概念,在不同的系統裡有可能面貌差異甚大。曾經引領數學風潮多年的法國布爾巴基(Bourbaki)學派,他們原想寫一套純數學集大成著作《數學原本》。1954年與1956年相繼出版了第一卷《集合論》的頭三章,打算用集合論做為講數學的基礎。因為受到希爾伯特形式化系統的影響,布爾巴基選擇了七個原始的基本符號,再經過繁複的堆疊引進其他符號與關係。於第三章第55頁的腳註裡,布爾巴基寫下了定義1的式子。同時說如果只用七個基礎符號把1的定義完整展開,大約需要數萬個符號。


布爾巴基這個「原則上」的估計數,實在大得夠嚇人。英國邏輯學家馬賽亞斯(A. R. D. Mathias)首次看到時想:「一定搞錯了吧,應該用幾百個符號就夠了。」於是他動手仔細計算布爾巴基定義展開後所用的符號總數。1999年馬賽亞斯公佈了他最終計算的結果,布爾巴基系統裡的1總共要用4523659424929個符號來定義。


布爾巴基所以會採納這套繁複的集合論系統,有其一定的時代背景,今日當然可用更簡便的系統來講集合論。其實布爾巴基學派在《數學原本》後續諸卷中都迴避直接使用自己的系統,並且在不同場合中流露出貶抑邏輯的態度。因為他們對歐洲數學界產生巨大影響,他們的偏見也間接窒礙了數學邏輯在歐洲的發展。時至今日,形式化的數學也許讓人消化不了,但是想要教會電腦推導數學真理,就沒辦法倚賴還未實現的電腦「直覺」了。處理天文數字長度的符號,原是電腦的看家本領。因此形式化便成為超出數值計算與資料處理,讓電腦進入數學推理的重要基石。