本書從計算的變遷這一獨特視角回顧了數學、邏輯學和哲學的歷史沿革,展
現了計算為數學研究發(fā)展帶來的全新前景,展望了這場數學革命在自然科學、信
息科學與哲學領域引發(fā)的重大變革。本書榮獲年法蘭西學術院哲學大獎,一直是數學、計算機科學和哲學領域的暢銷讀物。
一本榮獲法蘭西學術院哲學大獎的數學書
一本數學愛好者都應該讀一讀的哲學書
講述一段別開生面的數學歷程
引發(fā)一場改變科學面貌的哲學思考
展現算法時代,計算為自然科學與哲學研究帶來的震撼之力
數學踏上新的征程
人們常說,剛剛過去的一個世紀是數學真正的黃金時代。數學在 20 世紀的進步比先前所有的世紀加起來還要大。然而,剛剛開始的這個世紀也可能同樣是數學發(fā)展的好時候;蛟S,數學在這個世紀的變遷會和 20 世紀一樣巨大,甚至更為驚人。引發(fā)這種想法的信號之一是一場漸變:自 20 世紀 70 年代開始,數學方法的基石證明的概念逐漸發(fā)生演變,讓一個古老卻有些被人忽視的數學概念重新回到了舞臺中央,這就是計算。
計算能成為引發(fā)革命的導火索,這看起來有點不合常理。算法,比如做加法和做乘法的算法,常常被視為數學知識中最基礎的一部分,做計算也經常被看成是缺乏創(chuàng)造性的枯燥工作。數學家們自己對計算也頗有成見,勒內·托姆就曾說過:我的論述中很大一部分屬于純粹的猜想,大家基本上可以把它們看成是夢話。我接受這種定性……如今,世界上到處有這么多學者在做計算,難道有人做夢不是件好事嗎?用計算來做夢,大概還真有點難度啊……
不幸的是,對計算的偏見恰恰根植于數學證明這一概念的定義里。確實,歐幾里得以降,證明的定義就是利用公理和演繹規(guī)則構建的一套推理
。然而,要解決一個數學問題,僅僅需要構建一套推理嗎?數學的實踐難道沒有告訴我們,解決問題需要把推理的步驟和計算的步驟巧妙地融合起來嗎?公理化方法若局限在推理中,它所展現的數學視野恐怕也會十分狹隘。正是因為人們對約束過多的公理化方法多有批評,才讓計算有機會重新出現在數學的舞臺上,F在,已有一些研究工作(它們之間未必有關聯(lián))漸漸開始質疑推理高于計算的優(yōu)勢地位,并倡導一種更為平衡的觀點,讓兩者互為補充。
這場革命讓我們重新考量推理和計算之間的關系,同時也促使我們重新審視數學與物理學、生物學等自然科學之間的對話,特別是數學為何能在這些學科中發(fā)揮難以理解的強大作用這一古老問題,以及自然理論的邏輯形式這一全新問題。此外,這場革命給分析判斷和綜合判斷等哲學概念帶來了新的火花。它還讓我們反思數學與計算機科學之間的關系,而且數學似乎是唯一一門不需要借助機器的科學,它為什么如此獨特?
最后,最振奮人心的是,這場革命讓我們隱約看到了一些解決數學問題的新方式,它擺脫了過去的技術強加給證明長度的枷鎖數學也許正踏上新的征程,去探索從未涉足的全新領域。
誠然,公理化方法的危機并不是憑空出現的。從 20 世紀上半葉起就有許多先兆,特別是兩種理論可計算性理論和構造性理論的出現。這兩種理論本身雖然沒有質疑公理化方法,卻重新確立了計算在數學大廈中的地位。在討論公理化危機之前,我們會簡要回顧這兩個概念的歷史。不過,還是讓我們先上溯遠古,探尋計算這一概念的起源,看看古希臘人對數學的發(fā)明過程吧。
吉爾多維克(Gilles Dowek)
法國數學家、邏輯學家和計算機科學家,法國國家計算機與自動化研究所機器證明處理系統(tǒng)、編程語言、航空系統(tǒng)安全專家,美國國家航空研究院顧問。多維克撰寫過多部數學和計算機科學科普作品,曾榮獲法國數學學會達朗貝爾獎和法蘭西學術院哲學大獎。
第一篇 古老的起源
第1章 從史前數學到希臘數學 2
第2章 計算兩千年 17
第二篇 古典時代
第3章 謂詞邏輯 36
第4章 判定性問題與丘奇定理 56
第5章 丘奇論題 73
第6章 為計算樹立數學地位的嘗試λ演算 94
第7章 構造性 100
第8章 構造性證明與算法 113
第三篇 公理化危機
第9章 直覺主義類型論 122
第10章 自動化證明 132
第11章 證明檢驗 145
第12章 學界新進展 153
第13章 工 具 172
第14章 公理的終結? 187
結語 旅程的尾聲 190
附錄一 人物簡介 193
附錄二 參考文獻 208
索 引 212