Can you summarize the following document?
        
  不完備性定理適用於足夠複雜,可以表示自然數算術的形式系統,而這種形式系統是自洽的,可以被公理化的。這些概念的詳細含義會在後面給出。尤其是在一階邏輯的語境中,形式系統也被稱為"形式定理"。一般地,一個形式系統被定義為含有一組特定公理集合以及符號變換規則(或者是推導規則)的演繹工具。這樣的一個形式系統的例子是一階算術系統,在這個系統中,所有變數都代表為自然數。而在其他系統中,例如集合論,只有部分屬於形式系統的表述才表示了自然數算術。不完備性理論是關於這些形式系統中的形式可證明性,而不是關於非形式意義上的"可證明性"。 形式系統可能具有的性質如下,完備性、一致性和有效公理化的存在性。不完備性定理則表明任何蘊含皮亞諾算術公理的形式系統不能同時具有這三個性質。

  如果形式系統中的定理集是遞迴可列舉的集合(Franzén 2004, p. 112),那麼該形式系統是"有效公理化的"(也被稱為“生成定理的有效性”)。  這意味著,在原則上計算機程式能夠列舉出系統中所有的定理,而不列出任何非定理的陳述。皮亞諾公理和策梅洛-弗蘭克爾集合論 (ZFC) 都是有效生成定理的例子。  現在被稱為真算術的理論不僅有皮亞諾算術中關於整數的正確陳述,而且是自洽和完備的,並有足夠的運算公理。但是它的定理集不是遞迴可列舉的集合,因此也不滿足不完備定理的假設。

  哥德爾巧妙地利用了命題的“真值為真”和“含義為真”的區別,從而構造出了含義為真而真值不可證的命題,又避免了悖論的陷阱。形式邏輯系統的命題本身是沒有含義的。命題只有真值而沒有含義。公理命題的真值為真。其它命題的真值為真當且僅當該命題可以被證明,為假當且僅當該命題的非可以被證明。當形式邏輯系統被實際應用時,系統中的符號都被對映到實際概念上,從而有了語義。這種對映叫做一個模型。有了模型,命題就有了含義(語義)。例如,在ZF公理化集合論中,系統中的物件(object)被影射到“集合”這一概念,∈被對映到“屬於”這一概念就是模型的一個例子。而ZF公理化系統本身即使沒有模型也可以成立。如果換一個模型,形式系統沒變,只是它不再是集合論了。當然,ZF公理化系統是為了集合論量身打造的,很適合於集合論。如果換一個模型,很難找到可理解的語義。但這說明了“真值為真”和“含義為真”是有區別的。  在大多數情況下,命題的“真值為真”和“含義為真”是一致的。例如,設A為一命題,則命題A↔¬A的含義是“本命題A為假”,這時A的真值為真和含義為真是一致的,結果形成了否定迴圈而構成了悖論。而邏輯系統不能含有悖論,所以這樣的A應該是構造不出來的。哥德爾定理證明的巧妙之處就在於將悖論的“為假”改為了“為不可證”使得真值為真和含義為真成為不一致(含義為真是不可證,而真值為真或假都是可證),因而產生了自我否定又避免了迴圈的效果,也就避免了悖論。  理解了這一點,就可以理解哥德爾定理不是說存在真值為真又不可證這種自相矛盾的悖論命題(實際上應該構造不出來),而是存在含義為真但不可證(即真值不可知)的命題。哥德爾定理也不只是說存在既不可證真,也不可證偽的命題,這樣的命題有很多,哥德爾定理的重要之處在於它還說了該不可證的命題是含義為真的。  哥德爾定理是一階邏輯的定理,故最終只能在這個框架內理解。在形式邏輯中,數學命題及其證明皆以一種符號語言描述,只要檢查每一個證明的有效性,便可從一組公理開始無可辯駁地證明一條定理。理論上,這樣的證明可以在電腦上檢查,事實上這樣的有效性檢查程式也已經有了。  為了這個過程得以進行,需確定手頭有什麼樣的公理。可以從一組有限的公理集開始,例如歐幾里得幾何。或者更一般地,由一個可以允許無窮的公理列表開始,只要能機械地判斷給定的命題是否是一條公理就行。在電腦科學裡面,這被稱為公理的遞迴集。儘管無窮的公理列表聽起來有些奇怪,實際上自然數的通常理論中(被稱為皮亞諾公理)就是如此。  哥德爾的第一條不完備定理表明任何一個允許定義自然數的體系必定是不完備的:它包含了不能在此體系內以一階謂詞邏輯形式證明的命題,並且該命題的否命題也不能在該體系內以一階謂詞邏輯的形式證明。  存在不完備的體系這一事實本身並不使人感到特別驚訝。例如,在歐幾里得幾何中,如果把平行公設去掉,就得到一個不完備的體系。不完備的體系可能只意味著尚未找出所有必須的公理而已。  但哥德爾揭示的是在多數情況下,例如在數論或者實分析中,永遠不能找出公理的完整集合。換句話說,每一次將一個命題作為公理加入,將總有另一個命題出現在所能形式證明的範圍之外。  如果加入無窮條公理(例如,所有真命題)到公理列表中,確保所有命題都可證明為真或假,但得到的公理列表將不再是遞迴集。給出任意一條命題,將沒有機械的方法判定它是否是系統的一條公理。如果給出一個證明,一般來說也無法檢查它是否正確。  在電腦科學的語言中,哥德爾定理有另一種表述方式。在一階邏輯中,定理是遞迴可列舉的:你可以編寫一個可以列舉出其所有有效證明的程式。你可以問是否可以將結論加強為遞迴的:可以編寫一個在有限時間內判定命題真假的程式嗎?根據哥德爾定理,答案是一般來說不能。

  哥德爾和保羅·寇恩得出的一些結果結合起來給出了不確定命題(既不能證明也不能否證的命題)的一個實際例子:選擇公理和連續統假設都是集合論的標準公理系統內的不確定命題。  在1973年,同調代數中的懷特海問題被證明是集合論中的不確定命題。  1977年,Paris和Harrington證明了組合論中的一個命題,拉姆賽理論的某個版本,在皮阿諾公理給出的算術公理系統中是不確定的,但可以在集合論的一個更大體系中證明為真。  在電腦科學中用到的Kruskal的樹問題,也是在皮亞諾公理中不確定而在集合論中可證明的。  Goodstein定理是一個關於自然數的相對簡單的命題,它在皮亞諾算術中是不確定的。  古格里·錢頓(Gregory Chaitin)在演算法資訊理論中構造了一個不確定命題,即「Chaitin隨機數Ω的第n個位元組是否為0」這樣的命題在ZFC內是不可判定的。  計算邏輯中的停機問題不可解,亦是哥德爾不完備定理的一種表現形式。

  以下列出的誤解都是針對第一條定理而產生的。

  不完備性的結論影響了數學哲學以及形式化主義(使用形式符號描述原理)中的一些觀點。第一定理可以被解釋為:“不存在一個萬能的公理系統,使得其既能夠證明一切數學真理,又能證偽任何謬誤。” 以下對第二定理的另一種說法甚至更令人不安: 如果一個(強度足以證明基本算術公理的)公理系統可以用來證明它自身的相容性,那麼它是不相容的。 於是,為了確立系統S的相容性,就要構建另一個系統T,但是T中的證明並不是完全可信的,除非不使用S就能確立T的相容性。舉個例子,自然數上的皮亞諾公理的相容性可以在集合論中證明,但不能單獨在自然數理論範圍內證明。這對大衛·希爾伯特的著名的未解決的23個數學問題中的第二個給出了一個否定回答。  理論上,哥德爾理論仍留下了一線希望:也許可以給出一個演算法判定一個給定的命題是否是不確定的,讓數學家可以忽略掉這些不確定的命題。然而,對可判定性問題的否定回答表明不存在這樣的演算法。  值得注意的是,符合哥德爾不完備定理的系統,必須要蘊涵皮亞諾算術公理以承載對第一不完備定理證明過程的編碼。基本上,這就要求系統能將一些基本操作例如加法和乘法形式化,例如在魯賓遜算術Q中那樣。有一些更弱的公理系統是相容而且完備的,例如,它包括所有的一階邏輯的真命題和關於加法的真命題。  公理系統可能含有無窮條公理(例如皮亞諾算術就是這樣),但要哥德爾定理生效,必須存在檢驗證明是否正確的有效演算法。例如,可以將關於自然數的所有在標準模型中為真的一階語句組成一個集合。這個公理系統是完備的;哥德爾定理之所以無效,是因為不存在決定任何一條語句是否正確的有效演算法。從另一方面說,這個演算法的不存在正是哥德爾定理的直接結果。  另一個哥德爾定理不適用的特殊情況是:將關於自然數的所有語句首先按長度然後按字典順序排序,並從皮亞諾公理集開始,一個一個遍歷列表,如果發現一條語句既不能證明又不能否證,就將它作為公理加入。這樣得到的系統是完備的,相容的,並且是足夠強大的,但不是遞迴可列舉的。  哥德爾本人只證明了以上定理的一個較弱版本;以上定理的第一個證明是羅素(Russel)於1936年給出的。  基本上,第一定理的證明是通過在形式公理系統中構造如下命題  來完成的。這樣,它可以看成是說謊者悖論的一個現代變種。  如果公理系統是相容的,哥德爾證明了p(及其否定)不能在系統內證明。因此"p"是真命題("p"聲稱它不可證明,而它確實不能),儘管其證明不能在系統內形式化。請注意將p作為公理加入系統並不能解決問題:擴大了的系統中會有另一個哥德爾語句出現。  羅傑·彭羅斯聲稱“可被機械地證明的”和“對人類來說看起來是真的”的這一區別,表明了人類智慧在本質上不同於機械過程。這一觀點未被普遍接受,因為正如馬文·閔斯基所指出的,人類智慧有犯錯誤和理解不相容和謬誤句子的能力。但馬文·閔斯基透露說庫爾特·哥德爾私下告訴他,他相信人類有一種到達真理的直覺方法,但因為跟計算機式的方法不同,人類可以知道為真的事情並不受他的定理限制。  對以上認為該定理揭示了人類具有超出形式邏輯之能力的這種觀點,也可以作如下評論:"p無法被證明,也無法被證偽",因為無法知道系統是否是相容的。因此實際上我們並不知道系統之外的任何真理。我們所確知的只有這樣一個命題:  這樣的命題之前已經在系統內部被證明。實際上,這樣的證明可以如下給出。

  要充實對證明要點的描述,主要的問題在於:為了構造相當於“p是不可證明的”這樣的命題p,p就必須包含有自身的引用,而這很容易陷入無窮迴圈。而哥德爾為了避開無窮迴圈而產生的方法,後來被艾倫·圖靈用於解決可判定性問題。  首先,每個公式,或者說可形式化的命題都可以被賦予一個數,稱為哥德爾數。例如,假設形式系統有100個符號,用0至99對這些符號進行編碼,這樣,一個命題的公式就是一個位數為公式長度的100進位制的整數,同一個公式可以有多種不同的寫法,因此可以對應多個數,但每一個數要麼不對應任何公式,要麼只對應唯一的一個公式,可能有多個數對應同一個公式。因為系統包含所有正整數,因此也就涵蓋了所有的公式。而一個證明可以表示為一個有窮的命題序列,例如將推理過程表示為命題序列。用同樣的原理也可以將一個證明過程表示為一個正整數。當然,表示一個命題的正整數和表示一個證明的正整數具有不同的含義,因此不能混在一起。  像F(x)這樣的公式含有一個自由變數x,它們稱為命題形式。一旦x被一個特定的數代替,它就成為一個真正的,可證的特定命題。於是它要麼是在系統中可證明的,要麼可證偽。例如我們設定F(x)為:x是偶數,那當設x=2時F(x)是可證明的,而x=3時F(x)是可證。由於F(x)不是命題,因此不能被證明也不能被否證。但每一個命題形式F(x)都有一個哥德爾數,可用G(F)表示。自由變數x的選取G(F)無關。  通過小心地分析系統的公理和推理規則,可以寫下一個命題形式P(x),它表示x是系統中一個可以證明的命題的哥德爾數。形式描述如下:如果x是一個可證明命題對應的哥德爾數,P(x)就可被證明,而其否定"~"P(x)則不能。(儘管這作為一個證明要點來說已經足夠,但在技術上卻不太嚴格。請參見哥德爾和羅素的有關論文,關鍵字是“omega-consistency”。)  現在,重點來了:一個命題形式F(x)稱為不可自證的,當且僅當把命題形式F的哥德爾數G(F)代入F中所得的命題F(G(F))是不可證明的。這個定義可以形式化,於是可以構造一個命題形式SU(z),表示z是某個不可自證命題形式的哥德爾數。SU(z)的形式描述如下:  現在我們所要的語句p就可以如下定義:  直觀上,當問到p是否為真的時候,我們是在問:“不可自證這個特性本身是不可自證的嗎?”這很容易讓人聯想到理髮師悖論,那個理髮師只替那些不替自己理髮的人理髮:他替自己理髮嗎?  現在讓我們假定公理系統是相容的。  如果p是可證明的,於是SU(G(SU))為真,根據SU的定義,z = G(SU)就是某個不可自證命題形式的哥德爾數。於是SU就是不可自證的,根據不可自證的定義,SU(G(SU))是不可證明的。這一矛盾說明p是不可證明的。  如果p是可證偽的,則根據SU的定義,z = G(SU)就不是不可自證命題形式的哥德爾數。這意味著SU不是不可自證的。根據不可自證的定義,我們斷定SU(G(SU))是可以證明的,推出矛盾。這說明p的否定也是不可證明的。  因此,p既不可在系統內證明也不可在系統內否證。

  令p是如上構造的不確定命題,且假定系統的相容性可以在系統內部證明。我們已經看到,如果系統是相容的,則p是不可自證的。這個證明過程可以在系統內部形式化,因此命題“p是不可證明的”或者“"~"P(p)”可以在系統內證明。  但是最後一個命題就等價於p自己(而且這種等價性可以在系統內部證明),從而p就可以在系統內證明。這一矛盾說明系統是不相容的。

  有學者指出不完備定理和不確定性原理有某種聯絡。
在數理邏輯中,哥德爾不完備定理是庫爾特·哥德爾於1931年證明並發表的兩條定理。簡單地說,第一條定理指出: 這是形式邏輯中的定理,容易被錯誤表述。有許多命題聽起來很像是哥德爾不完備定理,但事實上並不是。具體例項見對哥德爾定理的誤解。