【專欄】康托爾、哥德爾、圖靈——永恒的金色對角線（8）

哥德爾的不完備性定理

然而，漫長的Y Combinator征途仍然并非本文的最終目的，對于Y combinator的構造和解釋，只是給不了解lambda calculus或Y combinator的讀者看的。關鍵是馬上你會看到Y combinator可以由哥德爾不完備性定理證明的一個核心構造式一眼瞧出來！

讓我們的思緒回到1931年，那個數學界風起云涌的年代，一個名不經傳的20出頭的學生，在他的博士論文中證明了一個驚天動地的結論。

在那個年代，希爾伯特的數學天才就像太陽的光芒一般奪目，在關于數學嚴格化的大紛爭中希爾伯特帶領的形式主義派系技壓群雄，得到許多當時有名望的數學家的支持。希爾伯特希望借助于形式化的手段，抽掉數學證明中的意義，把數學證明抽象成一堆無意義的符號轉換，就連我們人類賴以自豪的邏輯推導，也不過只是一堆堆符號轉換而已（想起lambda calculus系統了吧)。這樣一來，一個我們日常所謂的，帶有直觀意義和解釋的數學系統就變成了一個純粹由無意義符號表達的、公理加上推導規則所構成的形式系統，而數學證明呢，只不過是在這個系統內玩的一個文字游戲。令人驚訝的是，這樣一種做法，真的是可行的！數學的意義，似乎竟然真的可以被抽掉！另一方面，一個形式系統具有非常好的性質，平時人們證明一個定理所動用的推導，變成了純粹機械的符號變換。希爾伯特希望能夠證明，在任一個無矛盾的形式系統中所能表達的所有陳述都要么能夠證明要么能夠證偽。這看起來是個非常直觀的結論，因為一個結論要么是真要么是假，而它在它所處的領域/系統中當然應該能夠證明或證偽了（只要我們能夠揭示出該系統中足夠多的真理）。

然而，哥德爾的證明無情的擊碎了這一企圖，哥德爾的證明揭示出，任何足夠強到蘊含了皮亞諾算術系統（PA）的一致（即無矛盾）的系統都是不完備的，所謂不完備也就是說在系統內存在一個為真但無法在系統內推導出的命題。這在當時的數學界揭起了軒然大波，其證明不僅具有數學意義，而且蘊含了深刻的哲學意義。從那時起這一不完備性定理就被引申到自然科學乃至人文科學的各個角落…至今還沒有任何一個數學定理居然能夠產生這么廣泛而深遠的影響。

哥德爾的證明非常的長，達到了200多頁紙，但其中很大的成分是用在了一些輔助性的工作上面，比如占據超過1/3紙張的是關于一個形式系統如何映射到自然數，也就是說，如何把一個形式系統中的所有公式都表示為自然數，并可以從一自然數反過來得出相應的公式。這其實就是編碼，在我們現在看來是很顯然的，因為一個程序就可以被編碼成二進制數，反過來也可以解碼。但是在當時這是一個全新的思想，也是最關鍵的輔助性工作之一，另一方面，這正是“程序即數據”的最初想法。

現在我們知道，要證明哥德爾的不完備性定理，只需在假定的形式系統T內表達出一個為真但無法在T內推導出（證明）的命題。于是哥德爾構造了這樣一個命題，用自然語言表達就是：命題P說的是“P不可在系統T內證明”（這里的系統T當然就是我們的命題P所處的形式系統了），也就是說“我不可以被證明”，跟著名的說謊者悖論非常相似，只是把“說謊”改成了“不可以被證明”。我們注意到，一旦這個命題能夠在T內表達出來，我們就可以得出“P為真但無法在T內推導出來”的結論，從而證明T的不完備性。為什么呢？我們假設T可以證明出P，而因為P說的就是P不可在系統T內證明，于是我們又得到T無法證明出P，矛盾產生，說明我們的假設“T可以證明P”是錯誤的，根據排中律，我們得到T不可以證明P，而由于P說的正是“T不可證明P”，所以P就成了一個正確的命題，同時無法由T內證明！

如果你足夠敏銳，你會發現上面這番推理本身不就是證明嗎？其證明的結果不就是P是正確的？然而實際上這番證明是位于T系統之外的，它用到了一個關于T系統的假設“T是一致（無矛盾）的”，這個假設并非T系統里面的內容，所以我們剛才其實是在T系統之外推導出了P是正確的，這跟P不能在T之內推導出來并不矛盾。所以別擔心，一切都正常。

那么，剩下來最關鍵的問題就是如何用形式語言在T內表達出這個P，上面的理論雖然漂亮，但若是P根本沒法在T內表達出來，我們又如何能證明“T內存在這個為真但無法被證明的P”呢？那一切還不是白搭？

于是，就有了哥德爾證明里面最核心的構造，哥德爾構造了這樣一個公式：

N(n) is unprovable in T

這個公式由兩部分構成，n是這個公式的自由變量，它是一個自然數，一旦給定，那么這個公式就變成一個明確的命題。而N則是從n解碼出的貨真價實的（即我們常見的符號形式的）公式（記得哥德爾的證明第一部分就是把公式編碼嗎）。”is unprovable in T”則是一個謂詞，這里我們沒有用形式語言而是用自然語言表達出來的，但哥德爾證明了它是可以用形式語言表達出來的，大致思路就是：一個形式系統中的符號數目是有限的，它們構成這個形式系統的符號表。于是，我們可以依次枚舉出所有長度為1的串，長度為2的串，長度為3的串…此外根據形式系統給出的語法規則，我們可以檢查每個串是否是良構的公式（well formed formula，簡稱wff，其實也就是說，是否符合語法規則，前面我們在介紹lambda calculus的時候看到了，一個形式系統是需要語法規則的，比如邏輯語言形式化之后我們就會看到P->Q是一個wff，而->PQ則不是），因而我們就可以枚舉出所有的wff來。最關鍵的是，我們觀察到形式系統中的證明也不過就是由一個個的wff構成的序列（想想推導的過程，不就是一個公式接一個公式嘛）。而wff構成的序列本身同樣也是由符號表內的符號構成的串。所以我們只需枚舉所有的串，對每一個串檢查它是否是一個由wff構成的序列（證明），如果是，則記錄下這個wff序列（證明）的最后一個wff，也就是它的結論。這樣我們便枚舉出了所有的可由T推導出的定理。然后為了表達出”X is unprovable in T”，本質上我們只需說“不存在這樣一個自然數S，它所解碼出來的wff序列以X為終結”！這也就是說，我們表達出了“is unprovable in T”這個謂詞。

我們用UnPr(X)來表達“X is unprovable in T”，于是哥德爾的公式變成了：

UnPr(N(n))

現在，到了最關鍵的部分，首先我們把這個公式簡記為G(n)——別忘了G內有一個自由變量n，所以G現在還不是一個命題，而只是一個公式，所以談不上真假：

G(n):UnPr(N(n))

又由于G也是個wff，所以它也有自己的編碼g，當然g是一個自然數，現在我們把g作為G的參數，也就是說，把G里面的自由變量n替換為g，我們于是得到一個真正的命題：

G(g):UnPr(G(g))

用自然語言來說，這個命題G(g)說的就是“我是不可在T內證明的”?？?，我們在形式系統T內表達出了“我是不可在T內證明的”這個命題。而我們一開始已經講過了如何用這個命題來推斷出G(g)為真但無法在T內證明，于是這就證明了哥德爾的不完備性定理。

哥德爾的不完備性定理被稱為20世紀數學最重大的發現（不知道有沒有“之一”）現在我們知道為真但無法在系統內證明的命題不僅僅是這個詭異的“哥德爾命題”，還有很多真正有意義的明確命題，其中最著名的就是連續統假設[1]，此外哥德巴赫猜想也有可能是個沒法在數論系統中證明的真命題。

【注釋】

[1]在數學中，連續統假設是關于無限集合的可能大小的假設，這一假設是由康托爾于1877年提出。

（待續；此文的修訂版已收錄《暗時間》一書，由電子工業出版社2011年8月出版。作者于2009年7月獲得南京大學計算機系碩士學位，現在微軟亞洲研究院創新工程中心從事軟件研發工程師工作。）