哥德爾第一不完備定理的乙個不嚴謹的版本是：如果理論k是一致的，那麼存在乙個好式子g，⊢k
g不成立，⊢k
¬g也不成立。
當然，嚴謹的版本要對理論k有所限定，還要對「一致性」加以定義。但上述不嚴謹的說法就是哥德爾第一不完備定理的通俗解釋。哥德爾天才的地方在於他巧妙地證明了這點，他找到了這樣乙個好式子g。這樣的g長什麼樣子呢？不知道，但是哥德爾證明了存在這樣的乙個g，使得⊢g
⇔unp
rov(
g)，也就是說，g等價於「g無法被證明」。這就是通俗意義上去解釋哥德爾第一不完備定理時用的語句 – 構建乙個公式g，它的內容是g：g無法被證明。
哥德爾這個結論是要放在形式邏輯系統中的。一眼看過去，首先就會對unprov(g)這個式子產生疑問：這是k中的好式子嗎？怎麼能把g當成變數符號（項）放進unprov呢？這個問題的答案一點也「不玄乎」。哥德爾定義了哥德爾數，所以好式子g可以被「編碼」成哥德爾數q。注意，q是乙個正整數。既然q是乙個整數，那麼q¯
就是理論k中的乙個項（k至少是含等式的理論，有乙個常量符號0，再有乙個函式符號f1
1 。q¯
就是這個函式對0應用q次），因此unprov(g)實際上寫成k中的好式子就是un
prov
(q¯)
。那麼，問題又來了，unprov又是個什麼樣的好式子呢？這個就要利用前面的命題：任意原始遞迴關係都能在k中表達。所以，哥德爾就構造了這麼乙個原始遞迴關係pf(y, x)：y是乙個證明序列（即好式子序列）的哥德爾數，x是乙個好式子的哥德爾數，pf
(y,x
) 成立，當且僅當，y的終點是x。現在，既然pf
(y,x
) 原始遞迴，那麼它在k中可表達，記為rp
f(x2
,x1)
，它的意思硬要解釋的話，可以是「x1
在k中被序列x2
證明」。接著，哥德爾又構建了這麼個好式子np
f(x1
) ：(∀
x2)¬
rpf(
x2,x
1)，意思是：對於任意的x2
，它都不是x1
的證明，也即x1
不可證。
好了，有了這個奇葩的好式子np
f(x1
) 後，最後一步，哥德爾利用「對角線思想」，構造了乙個好式子g，使得g⇔
npf(
g的哥德
爾數¯¯
¯¯¯¯
¯¯¯¯
¯¯¯¯
¯¯¯¯
) 。他怎麼構造的呢？這個g又長什麼樣子呢？哥德爾是這樣玩的：他構造了乙個原始遞迴函式d(
u)，既然它原始遞迴，那麼可在k中表達，記為rd
(x2,
x1) ，然後構造
g ：(∀
x1)(
rd(x
2,x1
)⇒np
f(x1
))，這個g就滿足上面所說的條件。這裡面的函式d(
u)就是「對角線函式」，
u 是某個好式子的哥德爾數。在實際操作中，哥德爾就把g自己編碼成哥德爾數後扔進了d(
g的哥德
爾數¯)
。以上就是哥德爾證明第一不完備定理時用的把戲，真的是精采絕倫，讓人嘆為觀止。這個g⇔
npf(
g)具體是什麼，怎麼解釋，是否玄學，絲毫不影響它的形式意義。不管你怎麼理解這個定理的內容，哥德爾就證明了存在這麼個g，使得既沒有⊢k
g ，也沒有⊢k
¬g。這個結論不是通過g⇔
npf(
g)的「意**釋」來證明的，而是通過
k 的一致性來證明的，證明如：假設有⊢k
g，那麼就存在乙個證明序列，它的終點是g。這個證明序列的哥德爾數記為
r ， g的哥德爾數記為
q，那麼就有⊢k
rpf(
r¯,q
¯)。但是根據g⇔
npf(
g)，又能得出⊢k
¬rpf
(r¯,
q¯) ，違反了一致性，所以就證明了不可能有⊢k
g 。證明不可能有
\vashk¬
g 也採用類似的論述即可。
下一節筆記就具體討論，哥德爾是如何構建這一系列的遞迴關係、遞迴函式和好式子的。
數理邏輯3 形式數論1
這節開始跳到第三章，其實第二章還有好多內容，但冗長沉悶，也不知道後面是否能用上。所以，先跳到第三章，若需要用到第二章剩餘的內容，再跳回去。自然數和幾何，應該是人類最古老的兩大數學分支。所以，任何試圖建立數學根基的系統，都避免不了要對自然數系統進行 基礎化 何為自然數？自然數的加減乘除的本質是什麼？這...
數理邏輯之 正規化
今天開始說正規化。先介紹幾個概念。語義等值 令 和 是命題邏輯公式，我們稱 和 語義等值當且僅當 且 成立。記為 可滿足公式 給定命題邏輯公式 我們說 是可滿足的，如果存在 的一次求值使得 取值 true.文字 文字l 是指命題原子p或 p。l p p 析取子句 析取子句 d是若干個文字的析取 d ...
數理邏輯1 命題演算3
形式理論 formal theory 上一節給出了一套命題演算系統的語言，接下來我們就基於這套語言，定義乙個 公理化的命題演算系統 即 形式理論 我們感興趣的是假定一些wf已存在 公理 和一套推導規則，我們能推導出何種wf，或者說判定某些wf能否被證明。形式理論的目的就在於研究在不同公理和不同推導規...