哥德爾不完備定理是一個相當有趣的邏輯學發現，要了解他的意涵，要先考慮哥德爾的編碼

哥德爾數（Gödel number）是一種編碼方式，在一個算術系統裡面，當我們把每個字符都排成一個有限的列，我們可以幫每個字符都指定一個自然數。具體來說，我們可能會寫下

$\neg$ 是 $1$ ，其後設意義為「否定」
$\lor$ 是 $2$ ，其後設意義為「或」
$\lor$ 是 $2$ ，其後設意義為「且」

當有符號 $s_i (i \in \N)$ ，其對應的哥德爾數為 $n_i$ 。我們並不是真的關心具體的每個符號，我們做這件事的理由是為了表示哥德爾編碼。所以這裡要開始定義哥德爾編碼，首先先看一個簡單的例子：當有系統的公式符號排列 $s_1 s_{10} s_4$ ，我們說公式的哥德爾編碼為 $2^{n_1}\cdot 3^{n_{10}}\cdot 5^{n_4}$ 。

因此用函數 $\alpha(i)$ 指示一個公式的每個位置 $i$ 符號的 Gödel number，則哥德爾編碼確切的定義是

\prod_{i \in I}p_i^{n_{\alpha(i)}}

，也就是將質數以每個符號對應的哥德爾數為指數，將它們全部乘起來。這個辦法只是為了迫使每個公式有對應的編碼存在。我們用 $\overline{G}$ 記號表示公式 $G$ 的哥德爾數。

$\alpha$ 函數給出第 $i$ 個出現符號的在表中的位置。

在承認前述的系統 $P$ 下，可以開始描述。

Definition. substitution [math-0004]

$x[m/n]$ 表示將公式 $x$ 中哥德爾數為 $n$ 之符號換成 $m$ 的哥德爾數再求此替換後公式的哥德爾編碼。

例如 $\neg y[n/\overline{y}] = \overline{\neg n}$

Theorem. Gödel incompleteness [math-0003]

2023-08-30

存在形式上不能證明卻是真確、可寫下的公式
用系統證明自身的一致性會導致不可決定的公式也被證明

Proof

首先，用 $\exists x. x \vdash k$ 表示有哥德爾數為 $k$ 的公式在系統 $P$ 中得到證明，而 $x$ 是其演示

哥德爾有一段很長的論證（證明這是原始遞歸函數），來說明這是可以被 $P$ 表示的，這裡跳過了這部分論證。且這也是為什麼要求系統 $P$ 是具備算術能的，因為表示編碼需要自然數算術。

定義 $n = \lnot\exists x. x \vdash y[y/y]$ ，但 $y$ 是未知量，隨意給一個還沒被使用來編碼的數字即可，比如 $\overline{y}$ 。於是我們重寫成 $n =\lnot\exists x. x \vdash y[y/\overline{y}]$ 。

現在構造 $G = \lnot\exists x. x \vdash n[n/\overline{y}]$ ，求其哥德爾編碼 $\overline{G}$ 可以發現正是 $n[n/\overline{y}]$ 所表示的編碼，因為

n[n/\overline{y}] = \overline{\lnot\exists x. x \vdash n[n/\overline{y}]} = \overline{G}

因此用 $\overline{G}$ 替換 $G$ 中的 $n[n/\overline{y}]$ ，會得到

\lnot\exists x. x \vdash \overline{G}

可以發現 $G$ 的後設含義正是「有哥德爾編碼為 $\overline{G}$ 的公式沒有系統 $P$ 中的證明」，然而

假設 $G$ 可以在 $P$ 中證明為真，就告訴我們 $\overline{G}$ 對應的公式不存在任何演示可以於 $P$ 中證明，但那就是我們剛證明的公式 $G$ 。
假設 $G$ 可以在 $P$ 中證明為否，就導出 $\overline{G}$ 對應的公式在 $P$ 中有演示，但那就是我們剛證否的公式 $G$ 。

綜合可知這意思就是 $G$ 可證，若且唯若 $G$ 可證否，是故承認 $G$ 就是承認 $P$ 不一致；反之，若 $P$ 一致則 $G$ 形式上就不可決定。

巧妙的是，並不難看出 $G$ 的 meta 陳述是真確的，因為確實不存在任何整數作為編碼滿足這個性質。換句話說，存在形式上不能證明卻是真確、可寫下的公式，這就是第一不完備定理。接著根據第一不完備定理知道了 $G$ 的真確性，卻在 $P$ 中形式上不可決定，所以 $P$ 不能證明一個真確的算術公式，因此 $P$ 必定是不完備的，這就是第二不完備定理。

因此在 The Blind Spot: Lectures on Logic 中可以看到其陳述更加關注核心：對一個足夠編碼自己又一致的系統

存在一個真確的公式 $G$ 不可決定
系統證明自己具有一致性會連帶證明這個不可決定的公式，所以系統無法證明自己的一致性

換句話說，要關心的並不是具體如何構造上面陳述的編碼，而是這類系統編碼系統自身的普遍性問題。