Gödel incompleteness

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

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$ 必定是不完備的，這就是第二不完備定理。