哥德爾不完備定理的意義
哥德爾定理是一階邏輯的定理，故最終只能在這個框架內理解。在形式邏輯中，數學命題及其證明都是用一種符號語言描述的，在這裡我們可以機械地檢查每個證明的合法性，於是便可以從一組公理開始無可辯駁地證明一條定理。理論上，這樣的證明可以在電腦上檢查，事實上這樣的合法性檢查程式也已經有了。為了這個過程得以進行，我們需要知道手頭有什麼樣的公理。我們可以從一組有限的公理集開始，例如歐幾里得幾何。或者更一般地，我們可以允許無窮的公理列表，只要能機械地判斷給定的命題是否是一條公理就行。在計算機科學裡面，這被稱為公理的遞歸集。儘管無窮的公理列表聽起來有些奇怪，實際上自然數的的通常理論中，稱為皮亞諾公理的就是這么一樣東西。
庫爾特·哥德爾（Kurt Gödel，1906年4月28日－1978年1月14日），數學家、邏輯學家和哲學家。其最傑出的貢獻是哥德爾不完備定理和連續統假設的相對協調性證明。哥德爾的第一條不完備定理表明任何一個允許定義自然數的體系必定是不完全的：它包含了既不能證明為真也不能證明為假的命題。
存在不完備的體系這一事實本身並不使人感到特別驚訝。例如，在歐幾里得幾何中，如果把平行公設去掉，就得到一個不完備的體系。不完備的體系可能只意味著尚未找出所有必須的公理而已。
但哥德爾揭示的是在多數情況下，例如在數論或者實分析中，你永遠不能找出公理的完整集合。每一次你將一個命題作為公理加入，將總有另一個命題出現在你的研究範圍之外。
你可以加入無窮條公理（例如，所有真命題）到公理列表中確保所有命題都可證明為真或假，但你得到的公理列表將不再是遞歸集。給出任意一條命題，將沒有機械的方法判定它是否是系統的一條公理。如果給出一個證明，一般來說也無法檢查它是否正確。
在計算機科學的語言中，哥德爾定理有另一種表述方式。在一階邏輯中，定理是遞歸可枚舉的：你可以編寫一個可以枚舉出其所有合法證明的程式。你可以問是否可以將結論加強為遞歸的：你可以編寫一個在有限時間內判定命題真假的程式嗎？根據哥德爾定理，答案是一般來說不能。
不確定命題的例子
哥德爾和保羅·寇恩得出的一些結果結合起來給出了不確定命題（既不能證明也不能否證的命題）的一個實際例子：選擇公理和連續統假設都是集合論的標準公理系統內的不確定命題。在1973年，同調代數中的懷特海問題被證明是集合論中的不確定命題。
1977年，Paris和Harrington證明了組合論中的一個命題，拉姆賽理論的某個版本，在皮阿諾公理給出的算術公理系統中是不確定的，但可以在集合論的一個更大體系中證明為真。
在計算機科學中用到的Kruskal的樹問題，也是在皮亞諾公理中不確定而在集合論中可證明的。
Goodstein定理是一個關於自然數的相對簡單的命題，它在皮亞諾算術中是不確定的。
GregoryChaitin在算法資訊理論中構造了一個不確定命題,即``Chaitin隨機數Ω的第n個位元組是否為0"這樣的命題在ZFC內是不可判定的.
對哥德爾定理的一些誤解
由於哥德爾的第一條定理有不少誤解。我們舉出一些例子：該定理並不意味著任何有趣的公理系統都是不完備的。該定理需假設公理系統可以“定義”自然數。不過並非所有系統都能定義自然數，就算這些系統擁有包括自然數作為子集的模型。例如，歐幾里得幾何可以被一階公理化為一個完備的系統（事實上，歐幾里得的原創公理集已經非常接近於完備的系統。所缺少的公理是非常直觀的，以至於直到出現了形式化證明之後才注意到需要它們），塔斯基（Tarski）證明了實數和複數理論都是完備的一階公理化系統。
這理論用在人工智慧上，則指出有些道理可能是我們能夠判別，但機器單純用一階公理化系統斷卻無法得知的道理。不過機器可以用非一階公理化系統，例如實驗、經驗。
討論和推論
不完備性的結論影響了數學哲學以及形式化主義（使用形式符號描述原理）中的一些觀點。我們可以將第一定理解釋為“我們永遠不能發現一個萬能的公理系統能夠證明一切數學真理，而不能證明任何謬誤”以下對第二定理的另一種說法甚至更令人不安：
如果一個（強度足以證明基本算術公理的）公理系統可以用來證明它自身的相容性，那么它是不相容的。
於是，為了確立系統S的相容性，就要構建另一個系統T，但是T中的證明並不是完全可信的，除非不使用S就能確立T的相容性。舉個例子，自然數上的皮亞諾公理的相容性可以在集合論中證明，但不能單獨在自然數理論範圍內證明。這對大衛·希爾伯特的著名的未解決的23個數學問題中的第二個給出了一個否定回答。
理論上，哥德爾理論仍留下了一線希望：也許可以給出一個算法判定一個給定的命題是否是不確定的，讓數學家可以忽略掉這些不確定的命題。然而，對可判定性問題的否定回答表明不存在這樣的算法。
要注意哥德爾理論只適用於較強的公理系統。“較強”意味著該理論包含了足夠的算術以便承載對第一不完備定理證明過程的編碼。基本上，這就要求系統能將一些基本操作例如加法和乘法形式化，例如在魯賓遜算術Q中那樣。有一些更弱的公理系統是相容而且完備的，例如Presburger算術，它包括所有的一階邏輯的真命題和關於加法的真命題。
公理系統可能含有無窮條公理（例如皮亞諾算術就是這樣），但要哥德爾定理生效，必須存在檢驗證明是否正確的有效算法。例如，可以將關於自然數的所有在標準模型中為真的一階語句組成一個集合。這個公理系統是完備的；哥德爾定理之所以無效是因為不存在決定任何一條語句是否公理的有效算法。從另一方面說，這個算法的不存在正是哥德爾定理的直接結果。
另一個哥德爾定理不適用的特殊情況是：將關於自然數的所有語句首先按長度然後按字典順序排序，並從皮亞諾公理集開始，一個一個遍歷列表，如果發現一條語句既不能證明又不能否證，就將它作為公理加入。這樣得到的系統是完備的，兼容的，並且是足夠強大的，但不是遞歸可枚舉的。
哥德爾本人只證明了以上定理的一個較弱版本；以上定理的第一個證明是羅梭(Russel)於1936年給出的。
基本上，第一定理的證明是通過在形式公理系統中構造如下命題
p=“此命題是不可證明的”
來完成的。這樣，它可以看成是說謊者悖論的一個現代變種。
如果公理系統是相容的，哥德爾證明了p（及其否定）不能在系統內證明。因此p是真命題（p聲稱它不可證明，而它確實不能），儘管其證明不能在系統內形式化。請注意將p作為公理加入系統並不能解決問題：擴大了的系統中會有另一個哥德爾語句出現。
羅傑·彭羅斯聲稱“可被機械地證明的”和“對人類來說看起來是真的”的這一區別表明人類智慧型不同於自然的無意識過程。這一觀點未被普遍接受，因為正如MarvinMinsky所指出的，人類智慧型有犯錯誤和理解不相容和謬誤句子的能力。但MarvinMinsky透露說庫爾特·哥德爾私下告訴他，他相信人類有一種到達真理的直覺方法，但因為跟計算機式的方法不同，人類可以知道為真的事情並不受他的定理限制。
對以上認為該定理揭示了人類具有超出形式邏輯之能力的這種觀點也可以作如下評論：我們其實不知道p是真是假，因為我們並不（也無法）知道系統是否是相容的。因此實際上我們並不知道系統之外的任何真理。我們所確知的只有這樣一個命題：
要么p在系統內部無法證明，要么該系統是不相容的。
這樣的命題之前已經在系統內部被證明。實際上，這樣的證明已經給出。
第一不完備定理的證明要點
要充實對證明要點的描述，主要的問題在於：為了構造相當於“p是不可證明的”這樣的命題p，p就必須包含有自身的引用，而這很容易陷入無窮循環。將要介紹的哥德爾巧妙的把戲，後來被艾倫·圖靈用於解決可判定性問題。開始的時候，每個公式或者說可形式化的命題都被我們的系統賦予一個唯一的數，稱為哥德爾數。這要通過一種可以方便地在哥德爾數和公式之間（機械地）來迴轉換的方式來完成。因為系統足以表述“數”的概念，因此也就足以表述公式的概念了。公式可以為命題形式、命題或其他。命題形式的哥德爾數數值不同於命題的哥德爾數數值。
象F(x)這樣的公式含有一個自由變數x，它們稱為命題形式。一旦x被一個特定的數代替，它就馬上變成一個真正的特定命題，於是它要么是在系統中可證明的，要么不。命題形式自身並不是命題，因此不能被證明也不能能被否證。但每一個命題形式F(x)都有一個哥德爾數，可用G(F)表示。無論自由變數取什麼值，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)的形式描述如下：
對某個命題形式F(x)有z=G(F)，而且設y是命題F(G(F))的哥德爾數，則有~P(y)成立。
現在我們所要的語句p就可以如下定義：
p=SU(G(SU))
直觀上，當問到p是否為真的時候，我們是在問：“不可自證這個特性本身是不可自證的嗎？”這很容易讓人聯想到理髮師悖論，那個理髮師只替那些不替自己理髮的人理髮：他替自己理髮嗎？
現在讓我們假定公理系統是相容的。
如果p可以證明，於是SU(G(SU))為真，根據SU的定義，z=G(SU)就是某個不可自證命題形式的哥德爾數。於是SU就是不可自證的，根據不可自證的定義，SU(G(SU))是不可證明的。這一矛盾說明p是不可證明的。
如果p=SU(G(SU))的否定是可以證明的，則根據SU的定義，z=G(SU)就不是不可自證命題形式的哥德爾數。這意味著SU不是不可自證的。根據不可自證的定義，我們斷定SU(G(SU))是可以證明的，同樣得到矛盾。這說明p的否定也是不可證明的。
因此，p既不可在系統內證明也不可在系統內否證。
第二不完備定理的證明要點
令p是如上構造的不確定命題，且假定系統的相容性可以在系統內部證明。我們已經看到，如果系統是相容的，則p是不可自證的。這個證明過程可以在系統內部形式化，因此命題“p是不可證明的”或者“~P(p)”可以在系統內證明。但是最後一個命題就等價於p自己（而且這種等價性可以在系統內部證明），從而p就可以在系統內證明。這一矛盾說明系統是不相容的。
