跳轉到

1.3 Gödel 不完備定理：極限的發現，也是可計算性的誕生#

本節目標#

  • 掌握 Gödel 1931 年第一與第二不完備定理的精確陳述與證明思路（算術化、對角引理、Gödel 句子）。
  • 理解它們對 Hilbert 計畫的精確打擊範圍：殺死了什麼、沒殺死什麼。
  • 認識不完備定理同時催生「可計算性」概念，為 Turing 機鋪路的歷史辯證。
  • 鳌清常見誤解：不完備 ≠ 證明無法被機器檢查——這是理解 Lean 等證明助理的關鍵前提。

1931：一篇改寫基礎的論文#

1931 年，25 歲的 Kurt Gödel 發表〈論《數學原理》及相關系統中不可判定的命題〉（Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I）。論文針對的正是 1.2 節 Hilbert 計畫的核心假設：只要形式化夠強，數學就能同時是一致且完備的。

第一不完備定理：任何一致、遞迴可公理化、且足以表達自然數算術（如 PA、ZFC）的形式系統 \(T\) ，都存在句子 \(G\) 使得

\[ T \nvdash G \quad \text{且} \quad T \nvdash \neg G \]

\(G\) 為真（在標準模型 \(\mathbb{N}\) 中），但 \(T\) 證明不了它。完備性目標陣亡。

第二不完備定理：同一類系統 \(T\) 無法證明自身的一致性：

\[ T \nvdash \mathrm{Con}(T) \]

一致性目標（就系統內部而言）陣亡。 而「可判定性」則要等 1936 年由 Church 與 Turing 以更強的否定收場（1.4 節）。

證明思路一：算術化——讓數學談論自己#

Gödel 的第一個神來之筆：每個符號、公式、證明都可編碼為自然數（Gödel 編號）。於是「 \(x\) 是某公理的編碼」「序列 \(y\) 是對編碼為 \(z\) 的公式的一個合法證明」這些元數學性質，全部變成算術命題，可在 \(T\) 內表達：

\[ \mathrm{Prov}_T(p) \;:\Longleftrightarrow\; p \text{ 是句子 } \varphi \text{ 在 } T \text{ 中之證明的編碼} \]

這正是 Hilbert 元數學構想被反轉的時刻：Hilbert 用元數學研究形式系統，Gödel 則讓形式系統在內部重現元數學。

證明思路二：對角引理與自指句子#

對角引理（不動點引理）：對任意含一自由變數的公式 \(\psi(x)\) ，存在句子 \(G\) 使得

\[ T \vdash G \leftrightarrow \psi(\ulcorner G\urcorner) \]

其中 \(\ulcorner G\urcorner\) 是 \(G\) 自身的 Gödel 數。也就是說， \(T\) 能構造出「談論自己編碼」的句子。

取 \(\psi(x) := \neg\mathrm{Prov}_T(x)\) ，得到核心句：

\[ G \leftrightarrow \neg\mathrm{Prov}_T(\ulcorner G\urcorner) \]

直讀即為：「 \(G\) 不可被 \(T\) 證明。」 這是說謊者悖論的算術化版本，但這次不是悖論，而是一個合法的算術命題：

  • 若 \(T \vdash G\) ，則存在證明，故 \(\mathrm{Prov}_T(\ulcorner G\urcorner)\) 為真，得 \(T \vdash \neg G\) ， \(T\) 不一致。矛盾。
  • 若 \(T \vdash \neg G\) ，則 \(\mathrm{Prov}_T(\ulcorner G\urcorner)\) 為真，即 \(T \vdash G\) ，同樣矛盾。

故（若 \(T\) 一致）兩者皆不可證。對角引理的結構正是 1.1 節對角線法與 Russell 悖論的第三次登場：

對 Hilbert 計畫的打擊：精確但有限#

Hilbert 目標 結局 打擊者
完備性 死：任何夠強的一致系統都有不可判定命題 Gödel 1931（第一定理）
系統內證自身一致性 死： \(T \nvdash \mathrm{Con}(T)\) Gödel 1931（第二定理）
可判定性（Entscheidungsproblem） 死：無此機械程序 Church / Turing 1936
一致性可用更強方法證明 活：Gentzen 1936 用超窮歸納證 \(\mathrm{Con}(\mathrm{PA})\) Gentzen 1936
證明可被機械檢查 活，而且活得很好 ——

注意第二定理的細節：它禁止的是 \(T\) 在自身內部證 \(\mathrm{Con}(T)\) 。Gentzen 在 1936 年以良序 \(\varepsilon_0\) 上的超窮歸納證明了 PA 一致——用的方法強於 PA，但不構成循環。Hilbert 計畫不是被一劍封喉，而是被重新劃定疆界：系統不能自證清白，但元層的、更強的系統可以研究它。這種「系統層級、逐層反思」的視角，正是現代證明助理架構的縮影：Lean 的 kernel（小而可信）檢查由各種自動化策略（大而複雜）產生的證明。

同時，可計算性誕生了#

容易被忽略的辯證：不完備定理的證明需要「遞迴可公理化」這個概念——公理集必須能被機械地列舉， \(\mathrm{Prov}_T\) 必須是可計算的謂詞。Gödel 為了刻畫它，在 1931 年論文中定義了原始遞迴函數（並於 1934 年 Princeton 講課中，在 Herbrand 建議下給出一般遞迴函數定義）。

換言之，證明「數學有極限」的過程，逼出了「什麼是機械可計算」的精確定義。Gödel 句子中的 \(\mathrm{Prov}_T\) 是一個可計算謂詞；而「可計算」一旦被精確化，距離 Turing 機與停機問題只有一步（1.4 節）。從 1.1 的 Russell 悖論到 1.4 的 Turing 機，這條因果鏈：

集合論危機 → 公理化 → 形式化與元數學 → 不完備定理 → 可計算性 → 計算機 → 證明助理 → AI 數學證明

常見誤解：不完備 ≠ 機器不能檢查證明#

這是最需要鳌清的一點，因為它直接關係本書主題：

命題 真假 說明
「存在機器能判斷任意命題是否可證」 假 這是 Entscheidungsproblem 的否定（1.4 節）
「存在機器能驗證一個給定證明是否正確」 真 逐符號檢查是可計算的、機械的
「Gödel 句子 \(G\) 永遠無法被證明」 誤導 在 \(T\) 中不可證；在 \(T + \mathrm{Con}(T)\) 等更強系統中可證

關鍵在證明與驗證的不對稱：

  • 找證明：困難，一般而言不可判定（這是自動定理證明與 AI 的戰場）。
  • 查證明：容易，是有限符號串的機械檢查（這是 Lean kernel 的本職）。

Lean 的工作模式正是踩在這條線上：人類與 AI（如深度學習策略、LLM）負責「找」，kernel 負責「查」。不完備定理沒有封殺這個架構——它只是保證：再強的找證明系統，也會有它找不到的定理。這不是警告 AI 數學證明不能做，而是精確標示其工作永遠是「開放、分層、逐級增強」的。

小結與練習#

重點回顧#

  • 第一不完備定理：夠強的一致形式系統必有真而不可證的句子 \(G \leftrightarrow \neg\mathrm{Prov}_T(\ulcorner G\urcorner)\) 。
  • 證明的兩根支柱：算術化（元數學變算術）與對角引理（自指而不悖論）。
  • Hilbert 三目標全倒，但「更強系統證較弱系統」的分層結構存活，成為證明論與證明助理的架構原則。
  • 不完備定理催生「遞迴/可計算」概念，直接鋪路 Turing 機；「找證明難、查證明易」的不對稱是 Lean 架構的邏輯基礎。

練習#

  1. 解釋為何 Gödel 句子 \(G\) 不像說謊者悖論那樣造成矛盾，而只是「真但不可證」。差異在哪個環節？
  2. 設 \(T\) 一致。證明： \(T + \neg G\) 也是一致的（但它是 \(\omega\) -不一致的——查閱 \(\omega\) -consistency 的定義，這是 Gödel 原始版本的假設，Rosser 1936 將其減弱為單純一致性）。
  3. 用第二不完備定理說明：為什麼不能以「ZFC 證明 ZFC 一致」作為數學可靠性的最終依據。
  4. 寫出「找證明 vs. 查證明」各一個日常類比（如：樂透開獎 vs. 對獎），並說明類比在何處失效。
  5. 預習：Gödel 編號把公式變數字；Turing 將把「程序」變資料。比較這兩次「編碼」在思想史上的對稱性。