計算理論
但對公理化數學體系最精彩的一段歷史是,希爾伯特對公理化的問題與歌德爾不完備定理對數學可完全公理化的反證,以下是這段歷史的簡要說明。
20 世紀的大數學家 Hilbert 曾經於 1900 年提出的 23 個數學問題中提到一個問題,就是「是否能為數學系統建立證明法則,讓數學證明可以完全被計算出來」,後來歌德爾 (Godel) 在 1926 年證明了一階邏輯的完備定理,讓大家看到了一線曙光,但歌德爾在 1929 年又提出了一個數論系統的不完備定理,證明了有些定理無法透過計算程序證明。
歌德爾的研究,後來在電腦領域,被圖靈 (Turing) 重新詮釋了一遍,圖靈證明了「停止問題」是電腦無法 100% 正確判定的問題,這也開啟了後來計算理論的研究之河。圖靈也因此而成為計算理論領域的第一人,所以 ACM 這個組織才會將電腦界的最重要獎項稱為「圖靈獎」(Turing Award)。
可計算性
計算理論是資訊科學的理論基礎,主要探討電腦能力極限的問題,哪些是電腦有可能解決的問題,哪些是電腦無法解決的問題,以下是計算理論的兩大問題:
- 哪些問題是可計算的? (What can be computed?)
- 計算該問題需要花費多少時間與空間? (Given a problem, how much resource do we need to compute it ?)
問題是、到底有什麼問題是電腦絕對無法解決的,也就是《不可計算》的呢?
有的,電腦確實有無法解決的問題,像是《圖靈》的《停止問題》就是其中最著名的例子!
圖靈與停止問題
圖靈是計算理論的先驅,他在 1936年於「On Computable Numbers, with an Application to the Entscheidungsproblem」 這篇論文中提出了「圖靈機」的概念,並且證明了「停止問題」是任何圖靈機都無法完美解答的問題,以下是停止問題的簡單描述。
1. 請問您是否有辦法寫一個程式,判斷另一個程式會不會停,
2. 如果會停就輸出 1,不會停就輸出 0。
停止問題不可判定
由於圖靈的證明是建構在圖靈機上的,而圖靈機又很難用幾句話簡單描述,因此我們改用「現代程式」的方法證明停止問題,證明過程如下:
停止問題採用教數學的方式來說,是我們想定義一個函數 isHalt(code, data) ,
該函數可以判斷程式 code 在輸入 data 之後,是否會停止,
也就是 code(data) 會不會停止。
如我用程式寫下來,可寫成如下的演算法:
isHalt(code, data) = 1 假如 code(data) 會停就輸出 1
= 0 假如 code(data) 不停就輸出 0
但是、假如上述函數真的存在,那麼我們就可以寫出下列這個函數:
function U(code) // 故意用來為難 isHalt(code, data) 的函數。
if (isHalt(code, code)==1) // 如果 isHalt(U, U)=1,代表判斷會停
loop forever // 那 U 就進入無窮迴圈不停了,所以 isHalt(U,U) 判斷錯誤了。
else // 如果 isHalt(U, U)=0,代表判斷不停
halt // 那 U 就立刻停止,所以 isHalt(U,U) 又判斷錯誤了。
end
如此、請問 isHalt(U,U) 應該是甚麼呢? 這可以分成兩種情況探討:
1. 假如 isHalt(U, U) 傳回 1,那麼就會進入無窮回圈 loop forever,
也就是 U(U) 不會停
=> 但是 isHalt(U,U)=1 代表 isHalt 判斷 U(U) 是會停的啊?
於是 isHalt(U, U) 判斷錯誤了。
2. 假如 isHalt(U, U) 傳回 0,那麼就會進入 else 區塊的 halt,
也就是 U(U) 會立刻停止
=> 但是 isHalt(U,U)=0 代表 isHalt 判斷 U(U) 是不會停的啊?
於是 isHalt(U, U) 又判斷錯誤了。
於是、我們證明了停止問題是不可能做到 100% 正確的,
因為 isHalt 永遠對 U(U) 做了錯誤的判斷。
停止問題的意義
從上述的論證中,我們看到 isHalt(code, data) 這個問題是無法被 100% 正確解答的,因為這個問題與「羅素的理髮師問題」一樣,都是會導制矛盾的,因此我們可以根據「矛盾證法」的推論,發現這樣的問題是無法被「圖靈機或現代電腦」所正確解答的。
在 「韓非子/難一」 篇當中,曾經提到一個「矛與盾」的故事,原文截錄如下:
楚人有鬻楯與矛者,譽之曰︰『吾楯之堅,物莫能陷也。』又譽其矛曰︰『吾矛之利,於物無不陷也。』或曰︰『以子之矛陷子之楯,何如?』其人弗能應也。
現代電腦的能力基本上也只相當於一個記憶空間有限的圖靈機,因此一但證實了圖靈機無法解決某問題,那麼現代電腦也就無法解決該問題了。
相反的、假如我們可以證明「一個擁有無限記憶體的現代電腦」無法解決某個問題,那麼、應該也就可以證明圖靈機無法解決該問題了。
可證明性
在《電腦的領域》,程式人比較關心《可計算性》的問題,但是在《數學的領域》裡面,數學家們比較關心《可證明性》的問題。
但是、《可證明和可計算》兩者之間,其實有著非常緊密的關係。
上面的《圖靈停止問題》,是從《計算的角度》看一個問題是否可以用電腦完成。但是接下來,我們要改從數學家的角度,看看有那些問題是《可以被證明的》,又有那些問題是《無法被證明的》呢?
一致性與完備性
在邏輯系統中,所謂的《一致性》,是指公理系統本身不會具有矛盾的現象。假如我們用 A 代表該公理系統,那麼 A 具有一致性就是 A 不可能導出兩個矛盾的結論,也就是 A => P 與 A=> -P 不可能同時成立。
而完備性則是指一個公理系統,可以《推論出所有的在其中為真的定理》,不會有任何的遺漏,也就是《所有的定理都可以得到證明》的意思。
哥德爾於 1929 年證明了「哥德爾完備定理」(Gödel's Complete Theorem),這個定理較簡化的陳述形式如下:
- 一階邏輯系統是一致且完備的,也就是所有的一階邏輯定理都可以透過機械性的推論程序證明出來,而且不會導出矛盾的結論。
《哥德爾完備性定理》似乎得到了一個很正向的結果,讓人對邏輯系統的能力擁有了一定的信心。
現在就讓我們來看看《哥德爾完備性定理》到底是甚麼意思吧!
哥德爾完備性定理
哥德爾於 1929 年證明了「哥德爾完備定理」(Gödel's Complete Theorem),這個定理較簡化的陳述形式如下:
- 一階邏輯系統是一致且完備的,也就是所有的一階邏輯定理都可以透過機械性的推論程序證明出來,而且不會導出矛盾的結論。
以下是哥德爾完備定理的兩種陳述形式,詳細的證明方法請參考 Wikipedia:Original proof of Gödel's completeness theorem。
Theorem 1. Every formula valid in all structures is provable.
Theorem 2. Every formula φ is either refutable or satisfiable in some structure
哥德爾不完備定理
但是、當哥德爾進一步擴展這個邏輯系統,加入了《自然數的加法與乘法》等運算之後,卻發現了一個令人沮喪的結果,那就是《包含自然數加法與乘法的一階邏輯系統,如果不是不一致的,那就肯定是不完備的,不可能兩者都成立》。
1900 年,德國的偉大數學家希爾伯特 (Hilbert),提出了著名的 23 個數學問題,其中的第二個問題如下所示。
證明算術公理系統的無矛盾性 The compatibility of the arithmetical axioms.
在上述問題中,希爾伯特的意思是要如何證明算術公理系統的 Compatibility,Compatibility 這個詞意謂著必須具有「一致性」 (Consistency) 與「完備性」(Completeness)。
為此、許多數學家花費了一輩子的心力,企圖建構出一個「既一致又完備」的邏輯推論系統,像是「羅素與懷德海」就寫了一本「數學原理」,希望為數學建構出非常扎實的「公理系統」。
結果、這樣的企圖心被哥德爾的一個定理給毀了,那個定理就是「哥德爾不完備定理」。
要瞭解「哥德爾不完備定理」之前,最好先瞭解一下「邏輯悖論」這個概念。
當初、羅素在努力的建構數學原理時,卻發現了數學中存在著邏輯悖論,於是發出感嘆:「當我所建構的科學大廈即將完工之時,卻發現它的地基已經動搖了...」。
羅素的話,其原文是德文,據說翻譯成英文之後意義如下:
Hardly anything more unwelcome can befall a scientific writer than that one of the foundations of his edifice be shaken after the work is finished
結果,在 1950年,羅素穫得諾貝爾文學獎 (天啊!羅素不是數學家嗎!但是看他上面那句話的文筆,我很能體會他得諾貝爾文學獎的原因了 ...)
理髮師悖論
理髮師悖論可以描述如下:
在某一個小世界裏,有一個理髮師,他宣稱要為該世界中所有不自己理頭髮的人理髮,但是不為任何一個自己理頭髮的人理髮!
請問、他做得到嗎?
您覺得呢?
這個問題的答案是,他絕對做不到,原因出在他自己身上:
如果他「為」自己理頭髮,那麼他就為「一個自己理頭髮的人理髮」,違反了後面的宣言。
如果他「不為」自己理頭髮,那麼他就沒有為「該世界中 "所有" 不自己理頭髮的人理髮」,因此違反了前面的宣言。
於是、他理也不是、不理也不是,這就像中國傳說故事裏「矛與盾」的故事一樣,他的問題陷入兩難,產生「矛盾」了。
所以、該理髮師想做的事情是不可能做得到的!
這樣的悖論,在邏輯與電腦的理論裏有很深遠的影響,哥德爾正是因為找到了邏輯體系的悖論而發展出「哥德爾不完備定理」,而電腦之父圖靈也事發現了「停止問題」會造成悖論而證明了有些事情電腦做不到 ....
哥德爾不完備定理的描述
當初「哥德爾」提出的「不完備定理」,大致有下列兩種描述方法,後來簡稱為「哥德爾第一不完備定理」與「哥德爾第二不完備定理」,如下所示。
哥德爾第一不完備定理
定理 G1:若公理化邏輯系統 T 是個包含基本算術 (皮諾公設)的一致性系統,那麼 T 中存在一種語句 S,但是你無法用 T 證明 S ,卻也無法否證 S。
哥德爾第二不完備定理
定理 G2:若公理化邏輯系統 T 是個包含基本算術 (皮諾公設)的一致性系統,那麼 T 無法證明自己的一致性。
但是、對於「程式人」而言,上述描述都太邏輯了,讓我們改用「程式人」的角度來看這個問題,提出另一種「程式型版本」的說法:
哥德爾不完備定理的程式型:
定理 G3:不存在一個程式,可以正確判斷一個「包含算術的一階邏輯字串」是否為定理。
哥德爾不完備定理的程式型證明
接著、就讓我們來「證明」一下上述的程式型「哥德爾不完備定理」吧!
由於牽涉到矛盾,所以我們將採用反證法:
證明:
假如這樣一個程式存在,那麼代表我們可以寫出一個具有下列功能的函數。
function Proveable(str)
if (str is a theorem)
return 1;
else
return 0;
end
這樣的函數本身,並不會造成甚麼問題,「包含算術的一階邏輯」(簡稱為 AFOL) 夠強,強到可以用邏輯式描述 Provable(str) 這件事,因此我們可以寫出 Provable(s)
這樣一個邏輯陳述。
更厲害的是,我們也可以將一個字串在 AFOL 裏,是否為定理這件事情,寫成邏輯陳述 (註:邏輯符號 ∃ 代表存在,- 代表 not, & 代表 and, | 代表 or)。
接著、我們就可以問一個奇怪的問題了!那個問題描述如下。
請問 isTheorem(∃s -Provable(s) & -Provable(-s)) 是否為真呢?
讓我們先用 T 代表 ∃s -Provable(s) & -Provable(-s) 這個邏輯式的字串,然後分別討論「真假」這兩個情況:
如果 isTheorem(T) 為真,那麼代表存在無法證明的定理,也就是 Provable 函數沒辦法證明所有的定理。
如果 isTheorem(T) 為假,那麼代表 -T 應該為真。這樣的話,請問 Provable(-T) 會傳回甚麼呢?讓我們分析看看:
function Proveable(-T)
if (-T is a theorem) // 2.1 這代表 -(∃s -Provable(s) & -Provable(-s)) 是個定理,也就是 Provable() 可以正確證明所有定理。
return 1; // 但這樣的話,就違反了上述 「2. 如果 isTheorem(T) 為假」的條件了。
else // 2.2 否則代表 -T 不是個定理,也就是存在 (∃) 某些定理 s 是無法證明的。
return 0; // 但這樣的話,又違反上述「2. 如果 isTheorem(T) 為假」的條件了。
end
於是我們斷定:如果 Provable() 對所有輸入都判斷正確的話,那麼 2 便是不可能的,因為 (2.1, 2.2) 這兩條路都違反 2 的假設,也就是只有 1 是可能的,所以我們可以斷定 Provable(s) 沒辦法正確證明所有定理。
結語
在本文中,我們沒有寫出 Provable(s) 的邏輯陳述,也沒有寫出 isTheorem() 的邏輯陳述,因為這需要對「程式的指令集」,也就是 CPU 做一個邏輯描述,這樣說來故事就太長了!
而這個 CPU,通常後來的「計算理論」書籍裏會用「圖靈機」來描述,但這並不是哥德爾當初的證明,因為「哥德爾證明不完備定理」的年代,圖靈還沒有提出「圖靈機」的概念。
事實上、當初「哥德爾」的證明,根本也沒有「程式與電腦的概念」,所以「哥德爾」花了很多力氣建構了一個「哥德爾化的字串編碼概念」,這種字串編碼是建構在包含「+, *」兩個運算的算術系統上,也就是「皮亞諾公設」所描述的那種系統。這也是為何要引進「算術」到一階邏輯中,才能證明「哥德爾不完備定理」的原因了。
1931 年「哥德爾」證明出「不完備定理」之後,「圖靈」在 1936 年又提出了一個電腦絕對無法完全做到的「停止問題」(Halting Problem)。
「圖靈」的手法,與「哥德爾」非常類似,但是卻又更加簡單清楚。(不過既使如此,我還是很難直接理解圖靈的證明,因為本人在碩博士時連續被「圖靈機」荼毒了兩次,再也不希望跟「圖靈機」有任何瓜葛了 ....)
但是、我們仍然希望能夠讓「對程式有興趣」的朋友們,能夠清楚的理解「圖靈」與「哥德爾」在「計算理論」上的成就與貢獻,以免過於自大的想寫出一個「可以解決所有問題的程式」,我想只有站在前人的肩膀上,才能看清楚「程式」到底是個甚麼東西吧!
(當然、其實想要「寫出一個可以解決所有問題的程式」是非常好的想法。雖然「圖靈」與「哥德爾」已經都告訴過我們這是不可能的,但是身為一個程式人,就應該有挑戰不可能任務的決心,不是嗎? ........ 雖然、不一定要去做這種不可能的問題啦 ....)
參考文獻
- 康托尔、哥德尔、图灵——永恒的金色对角线
- 維基百科:謂詞邏輯
- 維基百科:一階邏輯
- 維基百科:二階邏輯
- Wikipedia:First-order logic
- Wikipedia:Second-order_logic
- 維基百科:哥德爾完備性定理
- http://www.encyclopediaofmath.org/index.php/Henkin_construction
- Wikipedia:Original proof of Gödel's completeness theorem
- Wikipedia:Russell's paradox
- 維基百科:羅素悖論
- An Outline of the Proof of Gödel's Incompleteness Theorem, All essential ideas - without the final technical details.
- Godel's Incompleteness Theorem, By Dale Myers
- 哥德尔轶事
- A Short Guide to Godel's Second Incomplete Theorem (PDF), Joan Bagaria.
- Wikipedia:Proof sketch for Gödel's first incompleteness theorem