多次提到彭羅斯將哥德爾不完備性定理(G?del's incompleteness theorems)作為核心論點之一，下面談一下全本（筆者）理解的這個定理及其意義。全本未必能用最嚴格的數(shù)學(xué)/邏輯定義來說明，同時全本也對一些問題存有疑問，但這里不影響對該定理框架的描述。證明和論述的來源：http://plato./entries/goedel-incompleteness/。

首先長話短說，這個定理的基礎(chǔ)是面向一組可數(shù)（通常是無限的，原因下面會簡述）的命題和推演的羅列（本來是集合，但因為有限/可數(shù)，所以就可以編序，這也是哥德爾定理的必需的基礎(chǔ)）。最能夠想象的也是這個定理本身所依靠的最小系統(tǒng)即皮亞諾算術(shù)公理系統(tǒng)(Peano axioms)。不清楚的話，只要想想可以不斷加一往上長的自然數(shù)和數(shù)學(xué)歸納法就是這個系統(tǒng)的最重要組成部分。對于命題和推演的集合在邏輯學(xué)上有一個比較牛逼的名稱叫形式系統(tǒng)(Formal System)。

在形式系統(tǒng)中大致可能會有以下這些內(nèi)容條目，

• 基本符號，比如a,b,數(shù)字之類。這些東西由于羅列和引用的意義不大，甚至可以被剔除。
• 基本符號的組合，包括代數(shù)式，函數(shù)等。因為不成為獨立的命題，也沒必要羅列。
• 命題（邏輯表達式）。在數(shù)學(xué)尤其邏輯學(xué)中，這經(jīng)常包括存在頭和任意頭。
• 含參命題（斷言）。在參數(shù)代入后，就變成命題。注意，這不同于函數(shù)，下面會談到。只含有一個參數(shù)的是一元命題，以下論證反復(fù)用到。
• 公理。就是這個系統(tǒng)認為真的基本條款。公理和邏輯推演是這個形式系統(tǒng)一致性發(fā)展的基礎(chǔ)。
• 推演式（真命題），就是把存在推演關(guān)系邏輯表達式串起來。如果是基于公理推演的，那么就是真命題（定理）了，這也是比較有意義的部分。如果是基于純邏輯的（比如a^b=>a），也不是不可以，但是意義不很大，空推有什么好推的。

需要注意的是，我們這里的系統(tǒng)，通常是無限的。原因是我們考慮系統(tǒng)的完備性，所以各種符號組合的可能性都需要考慮。所以任何一個能夠給出的合法的符號組合，尤其是命題，它必須必然需要被包括在內(nèi)。同理含參命題也一樣。

這個有點像什么？打個比方，我們在學(xué)校里學(xué)數(shù)學(xué)，做證明題，有的證明題那個難啊，還有什么奧數(shù)什么的。但在這里，我們可以設(shè)想有一部機器不斷依照一定順序地制造基本符號組合，從短的到長的，按照字典序什么的（以下的細化討論用了這個方案），這樣對于任意固定長度的符號序列，它總能被觸及到，只是早晚問題，而我們這里是邏輯/理論數(shù)學(xué)上討論的，這是理想機器，只要序列有限，都是“秒完成”（只有可行/不可行的問題，不存在什么運算復(fù)雜性之類的問題）。當然有一個“算法”可以檢查并確保生成的是合法的序列。然后這么一條條地生成，那么很顯然任何一個證明，無論多艱深，只要是有限的（廢話，證明當然是有限的），都無一例外能最終被羅列到?。ǖ?，這個系統(tǒng)本身不一定能確認之，有的能，有的不能，這是后面要說明的中心問題）

所以，雖然條目可以是無限的，但是可數(shù)的。所以我們能將這些條目編號。這個編號很有講究，編法當然不是唯一的，就像證明“自然數(shù)和有理數(shù)一樣多”，編法不對是出不了結(jié)果的。一個合法的編號就是能夠羅列出所有合法的符號組合。比方講，如果我們知道有一個東西是可數(shù)但無限的，比如自然數(shù)（雖然自然數(shù)作為簡單符號不編也沒關(guān)系），你就不能盯著它編，這樣你就編不了別的東西了。至少要夾花編。

其實我們會發(fā)現(xiàn)，無論從邏輯討論還是對于哥德爾定理的討論，很多條目邏輯上不必關(guān)心，當然真要編進去，只要編號合理也無傷大雅。我們比較關(guān)心的包括以下這些：

• 公理（無參真命題）
• 推演式（無參真命題）
• 無參命題
• 一元含參命題：A(x)

其中一元含參命題A(x)需要講一下。它不同于返回真假值的邏輯函數(shù)，它只是一個對參數(shù)的斷言，比如A(x):=x如何如何。當參數(shù)代入后，它退化為無參命題，則是有一個真假，這個由系統(tǒng)（論證鏈）來決定。它和邏輯函數(shù)的關(guān)系是：

• 如果有一個一元邏輯函數(shù)f(x)，則“f(x)=真”就是一個一元含參命題，當然“f(x)=假”，“f(x)=g(x)”也都是。
• 如果一個含參命題A(x)，對于每一個x的實例，在系統(tǒng)中都能找到A(x)或!A(x)的證明，那么我們也就得到了一個x到真/假的映射，即邏輯函數(shù)f(x)。
• 對于一個一元邏輯函數(shù)f(x)，如果系統(tǒng)能夠證明“對任意x如果f(x)則有A(x)否則!A(x)”，那么我們知道f(x)是個關(guān)于A(x)的“真函數(shù)”（實現(xiàn)）。

既然有了編號，我們對這個系統(tǒng)中任意一個條目m, 我們有它的一個編號[m]（別處用上方括號，這里簡便起見用一般方括號），我中文里稱它為m門，當然這是一個自然數(shù)。這里定義如果自然數(shù)[m] = n，則 = m。

接下來我們來看幾個比較有趣的函數(shù)和命題。注意這里的函數(shù)未必編號在系統(tǒng)中，只是對命題起到一個輔助（例如4和5）。

• “證明成立”函數(shù)P([a],[b])：如果a是b的一個證明則返回真，否則為假。注意這里編號的一個作用是用作為條目的ID，函數(shù)一般形式是接收自然數(shù)，這樣形式上比較統(tǒng)一（雖然函數(shù)內(nèi)部實現(xiàn)是去引用那兩個條目的，所以從計算機科學(xué)上講，這還是完完全全的函數(shù)式）。在表達正則化的前提下，這個函數(shù)的實現(xiàn)大意還是簡單的，只要比較命題和推演式的結(jié)論。顯然如此“實現(xiàn)”，這個函數(shù)成為一個真函數(shù)（不和這個系統(tǒng)矛盾）。
• “證明存在”含參命題Prov([b])：系統(tǒng)中存在條目b的證明。有沒有對應(yīng)函數(shù)實現(xiàn)（即對任意b可證與否命題成立）？最簡單幼稚的實現(xiàn)，顯然就是遍歷所有的條目調(diào)用P([a],[b])即可。當條目有限，則完全沒有問題，（無參）條目無限可數(shù)就麻煩了，因為除非有“洞察力”或特定的前提條件，否則永遠不能保證證明不在后面，所以是個停機問題。這是即便在形式系統(tǒng)中也是不允許的，因為證明必須是有限表達的。所以在系統(tǒng)中要實現(xiàn)這個，辦不到。所以我們在進行形式邏輯生成的時候，是換一個思路的。如果存在一個推演式最后有 =>b，那么就可以加一條Prov([b])是定理。實際系統(tǒng)中必然還有一個定理：對任意b，存在定理' ...=>b' <=> Prov([b])，由它推出上面的伴隨定理。
• “證明不存在”含參命題NoProv([b])（相當于!Prov([b])，但注意不是證偽b）：系統(tǒng)中不存在條目b的證明。是上面的否命題。
• “跳代”函數(shù)subst([a],n)：如果a是一個一元函數(shù)a(x)，則這個函數(shù)返回的是[a(n)]，即用n實例化a后的無參命題的編號。當然如果a不是一元函數(shù)，則異常返回（例如負數(shù)）。這個函數(shù)依賴編號系統(tǒng)有明確的“實現(xiàn)”。
• “跳代檢查（測試）”含參命題S([a],b,c)：a是一個一元函數(shù)且[a(b)] = c。相當于命題：subst([a],b)=c。這個命題在依賴編號系統(tǒng)有明確的“函數(shù)實現(xiàn)”（即調(diào)用subst：func_s(x,y,z) { return subst(x,y)==z; }）。

但是，我們會發(fā)現(xiàn)，如果對編號系統(tǒng)及其作用不進行比較嚴格的限定，這個問題的一致性討論是會成問題的。于是我們再對編號和編集進行如下細化，

我們假設(shè)系統(tǒng)的符號有限。于是我們可以將系統(tǒng)的條目進行字典排序，于是依此的羅列產(chǎn)生的可數(shù)集完成對所有可能的條目的羅列。在未經(jīng)說明之前，這個“可數(shù)集”就是“系統(tǒng)”的代名詞，可互換使用。
我們不特別使用=>符號（根據(jù)后面的討論可以容易地發(fā)現(xiàn)使用之是沒有必要的），于是推演式剔除，系統(tǒng)的條目精簡為僅含有公式（即命題，或前面說的“聲明”。它根據(jù)一定依據(jù)可以為真或假），當然含參公式必須允許，否則無法完成哥德爾矛盾的構(gòu)筑。當然系統(tǒng)還要包含公理，公理中必須包含邏輯公理從而可以實現(xiàn)推演。公理是有限的，排在系統(tǒng)之首，位于字典序的其他條目之前。公式包含Prov()。而Prov()依賴的Prv(,)二元含參公式則作為一個實用函數(shù)沒有實際用途，但作為合法條目可以存在于系統(tǒng)中（正如一元含參公式）。
我們必須假設(shè)存在一個“算法1”可以判決條目是否是“語法”合法的公式（因為Prv(,)等后續(xù)公式必然作用于語法合法的公式，所以我們必須認定這個“算法”存在），如果這個可數(shù)集包含不合法的公式。但這個“算法1”的存在性和可以構(gòu)造一個不含不合法公式的可數(shù)集是等價的。于是由“算法1”存在，我們可以過濾去無意義的條目。但我們可能對“語法”合法這個概念存在疑問，于是我們不得不假設(shè)包含“算法1”的“算法2”存在。
這樣可數(shù)集中的條目除了公理就是公式（含參或不含參）。
接下來外于這個可數(shù)集，我們有一個“算法2”，它能夠根據(jù)集合的內(nèi)容確定一個公式是否為真。對于含有->的公式，如果基于公理，就可以直接成真，這個式子實際是一個證明。這個“算法2”能夠“檢測”出此，而將這個邏輯式條目標記為真。就如上一個“算法1”能將語法非法的濾除，這個“算法2”則可判真（如果“算法1”的存在性存在疑問，我們必須假設(shè)“算法2”承擔“算法1”的功能）。同樣我們設(shè)定這個算法是“超越的”，即作用于整個可數(shù)集瞬間完成的。
注意，這樣的假設(shè)未能指出這個“算法2”必能把真命題都找出來，因為它是基于公理和推演式的。（但是希爾伯特規(guī)劃則顯然需要這個“算法2”具有這個能力，否則我們就已經(jīng)達到我們要否證的目的）。于是我們要假設(shè)“算法2”最終找出所有的真命題。原則上這個“算法2”和Prov()是要一致的，但哥德爾定理要說明這個一致性不存在。

至此，我們需要的基礎(chǔ)設(shè)施有了。接下來要導(dǎo)出哥德爾定理，主要靠對角線引理。這個方法就是康托(Georg Cantor)在論證無理數(shù)多于有理數(shù)中使用的著名的方法。只是在這里不是那么直觀而已。

這個引理結(jié)論很簡單：

【對角線引理】

對任意上述“自稱完備”的系統(tǒng)（有一定的基本限定條件，例如納入編號函數(shù)相關(guān)條目；不自稱完備則不用證明，因為已經(jīng)不完備），對于任意合法編號，對其中任意一個一元命題A(x)（簡稱A邏輯），都存在一個（依賴于編號函數(shù)的）D條款，使得D<=>A([D])。

根據(jù)這個引理，那么如果將A設(shè)為證明不存在函數(shù)NoProv()，就會出現(xiàn)D<=>NoProv([D])，即：

• D如果成立，它能導(dǎo)出NoProv([D])，也就是說證明了NoProv([D])，即證明了D是不能證明的；
• D如果不成立，它能導(dǎo)出!NoProv([D])，也就是Prov([D])，即證明了D是能夠證明的。

這顯然是一個矛盾，也是哥德爾定理揭示的問題。

要分析理解這個現(xiàn)象，我們先看這個引理是怎么來的。以下是這個對角線引理的證明。

【對角線引理證明】

首先我們看跳代檢查聲明S([a],b,c)，所有參數(shù)顯然都是自然數(shù)，雖然第一個參數(shù)的含義是對函數(shù)的引用，故而這里一開始用[a]標出作為提示。所以跳代檢查函數(shù)本身實際是S(x,y,z)。我們可以設(shè)想其一個特殊的實例S(x,x,y)，即對每一個一元函數(shù)（編號為x），跳代檢查聲明這個函數(shù)編號代入函數(shù)本身產(chǎn)生的無參命題的編號是y。這里實際做的是subst(x,x)，這稱作自跳代。

然后我們構(gòu)造一個一元命題B(x):=存在y使得A(y)^S(x,x,y)，簡稱B邏輯。容易看出，這個命題含義是對一個一元函數(shù)（編號為x）進行聲明，其自跳代（編號）代入一元邏輯函數(shù)A()得到的不含參命題為真。

由于B(x)本身也是一個一元函數(shù)，我們考慮將其代入B(x)自身（參數(shù)x設(shè)為B(x)本身的編號），即自跳代subst([B(x)],[B(x)])，亦即B([B(x)])。自然這是一個不含參命題，可將其記作D。從B(x)的定義看，這個自跳代D=B([B(x)])考察了（等價于）B(x)的B邏輯值，亦即B(x)的自跳代（編號）（亦即[D]）代入A()得到的命題。從而有D<=>A([D])。證畢。

接下來我們看為什么它是對角線，從而能看出這個引理的“幾何特征”。

首先我們列一個表，每一行的行號和每一列的列號對應(yīng)于相應(yīng)的哥德爾編號，均向著無限伸展。對于m行n列元素，假設(shè)m是一元邏輯命題M(x)的哥德爾編號（即[M(x)]=m），則這個元素為M(n)（對于不是一元命題的行，我們忽略，或標記一個負數(shù)之類即可）。于是上述（將NoProv()作為A()代入后的）B(x)就在[B(x)]=b行。然后我們再來看對角線，它實際上都是上述的自跳代 。最后我們看b行b列的元素。這個元素值，作為對角線上元素，它代表B(x)的自跳代命題；作為b行的元素，它代表（作為NoProv()的參數(shù)的）“B(x)的自跳代命題”不可證明這一命題。所以說這兩者是同一個條目。（即D==A([D])，這和上面的D<=>A([D])表述并不矛盾，實際上是一致的。“D<=>A([D])”本身是基于邏輯推演的真命題）

接下來我們再用更通俗的語言來看看B([B(x)])是怎么回事。B(x)是聲明：自己（x）對自己關(guān)于某件事是真的是不可證明的（和其他一元命題一樣，對每個具體的x，其真假與否由系統(tǒng)決定）。問題就是，B(x)自己說自己呢？（這個直接導(dǎo)致矛盾，系統(tǒng)也愛莫能助）

具體來看：

 : 存在y，!Prov(y)^S(x,x,y)       （即以!Prov為A的的B(x)一元含參公式）
 : 存在y，!Prov(y)^S(b,b,y)       （即以!Prov為A的D公式） （注意有且僅有g(shù)使得S(b,b,g)為真）
通俗地說是：一個人（他對各個人會有個聲稱）對它自己的聲稱，是無法證明的。而通俗地說是：（因為本身也是在對各個人做聲稱）說他自己（說的這話），是無法證明的，但這個無法證明又被他自己聲明為真的。

其實我們可以用這個方法構(gòu)造一個更簡單的矛盾：

 : 存在y, !^S(x,x,y)
 : 存在y, !^S(b',b',y)  （注意有且僅有g(shù)'使得S(b',b',g')為真）

這里通俗地說：一個人（它對各人會有個聲稱）對它自己的聲稱，總是假的（關(guān)于自己的話都是假的）。而通俗地說是：（因為本身也是在對個人做聲稱）說他自己說的這話，也是假的。但如果這是假的，那它又變真了。

注意這里的討論幾乎語義上對這個矛盾賦予了新的意義，從而幾乎脫離了編號系統(tǒng)。這個其實是有點像“我在撒謊”或羅素悖論，而的確哥德爾定理的確和羅素悖論結(jié)構(gòu)上有相通之處（對角線引理）。所以，一種觀點可以認為，哥德爾定理只不過是一個邏輯笑話。

上述需要注意的是，B(x)本身，對于不同x的實例，既有可能是真（可證明），也有可能假（可否證）。比如，在一個編號系統(tǒng)中，如果第2條是含參命題：x是偶數(shù)；而第四條是含參命題：x是奇數(shù)。那么B(2)就是假的，B(4)就是真的。

那么B([B(x)])到底是真是假呢？我傾向于認為：

它是真的（因為出了系統(tǒng)我們知道系統(tǒng)給不出它的證明，因為如果系統(tǒng)給出它的證明，系統(tǒng)就不一致了）。但是系統(tǒng)不能給出證明（或者等價地，否證）（但是系統(tǒng)連這個結(jié)論也無法作出），也就是在系統(tǒng)的觀點上無法知道其真假。

系統(tǒng)本身要是一致的，那么它至少其中會有一條如是的命題，它是真的，但是系統(tǒng)本身無法證明。而系統(tǒng)要一致，又必須去除這條矛盾的命題。所以系統(tǒng)是不完備的。

哥德爾定理給出的這種真的，但系統(tǒng)無法證明的命題，是利用了“證明”斷言構(gòu)筑的命題。但這構(gòu)筑是合法的。

但這不是系統(tǒng)中唯一的這類命題（真卻無法證明）。其他的這類命題（也是關(guān)于皮亞諾算術(shù)系統(tǒng)的）著名的如古德斯坦定理（Goodstein's Theorem）。

但是問題還沒完。正如某邏輯學(xué)家（名字忘了）說的，哥德爾定理有一難，一容易。一難是很難理解，一容易是很容易，其實極其容易誤解。就上面這段論證和說明的思路，不同的邏輯學(xué)家和相關(guān)學(xué)者都有不同的解釋。最關(guān)鍵的一點是關(guān)于這個證明存在含參命題Prov()的意義和存在方式，以及由此引申的關(guān)于彭羅斯的“數(shù)學(xué)洞察力”的問題。

筆者的一個想法/思路/對上述問題的看法是（不嚴格但不完全離譜）：重申這里Prov()的存在必須從邏輯學(xué)角度來理解，但是它具有深刻而微妙的“計算”牽連。從邏輯一致性上講，很顯然Prov()本身作為一個邏輯聲明其為真的充要條件是系統(tǒng)中存在證明鏈（語句）。而從機械（計算）“實現(xiàn)”的角度，它要求一個遍歷。這對于一個（在有限位置）真存在證明鏈（或證偽鏈也一樣）問題不算太大，但對于系統(tǒng)本身無法給出的證明呢？這從遍歷是無法實現(xiàn)的。于是我們必須假設(shè)系統(tǒng)的Prov()具有超出這種機械方法的能力，即如果一個證明存在，Prov()當然要反應(yīng)出來；而證明不存在，Prov()也反應(yīng)出來（即為非）（即使如果用“計算”無法發(fā)現(xiàn)這一點）。但這么一來，這個系統(tǒng)就真有無法證明的命題了（不管是真的還是偽的），而由此，由于偽命題的反命題就是真命題，于是系統(tǒng)就肯定無法證明的真命題，從而系統(tǒng)不完備。那我們只能假設(shè)這個系統(tǒng)能夠證明所有問題，也就是說Prov()對真命題返回真，對偽命題返回假，而不存在不能證明的命題。至于這個假設(shè)有沒有問題——其實這應(yīng)該是很有問題的，如果能導(dǎo)致矛盾（反證法），那我們會及早發(fā)現(xiàn)這個問題從而得出“系統(tǒng)總存在無法證明的真命題”——我們暫時不去管他（等于我們將對這個系統(tǒng)的要求放松很多/將這個系統(tǒng)的機能提高了很多）。但哥德爾定理這時候就基于Prov()構(gòu)造出了一個會使得這個系統(tǒng)形成矛盾的命題。在邏輯上這時候唯一的一個嘗試的是通過將上述D（一般文獻中稱為G_F。其中F是系統(tǒng)的代號，G代表哥德爾，即這個G_F是系統(tǒng)F的哥德爾命題）直接列為公理，但如此，很顯然，Prov()如果要有效，就會認定D可證明（公理本身是“0級證明鏈”），但D可證明直接導(dǎo)致D為否。筆者這里認為，邏輯上說，這說明Prov()是無效的或者說邏輯一致的Prov()是不存在的。總之筆者認為這足以說明一個機械系統(tǒng)（非但）總存在無法證明的（真）命題，其實根本不存在一個它自己能可靠掌握的（一致的）證明聲明Prov()，（從而引申到）更別提它能理解證明是怎么回事了。而這正是彭羅斯需要的。

在進一步細究之前，我們來看更詭異的哥德爾第二定理。

第二定理根據(jù)上述第一定理其過程看似很簡單。第一定理實際產(chǎn)生了一個真聲明（定理）：如果一個系統(tǒng)是一致的，則F不能包含G_F（即上述D）。這個定理在系統(tǒng)F中有一個證明鏈（當然這個證明鏈是難以想象的復(fù)雜的）。于是在這個系統(tǒng)中一個不一致的聲明X比如算式0=1，其不可證的聲明為!Prov(X)，另記作Cons(F)。Cons(F)要求系統(tǒng)一致，從而Cons(F)導(dǎo)出G_F，但這與第一定律矛盾，從而Cons(F)也不成立。

（未完待續(xù)）

補充閱讀

[1] 圖靈機的局限性的討論 （A Brief Review on a Limiatation of Turing Machine）