跳轉到

9.2 構造性證明與計算內容#

本章導言#

直覺主義的定理與經典數學的定理，表面陳述相同，內容不同：構造性證明附帶算法，經典證明可能不附帶。1945 年 Kleene 的可實現性詮釋把這個直覺精確化：Heyting 算術的證明可以「實現」為遞迴函數。1970 年後，Curry–Howard 對應（9.3 節）把「證明即程式」變成原理。本節講構造性證明的計算內容如何被提取：從 Gödel–Gentzen 翻譯到可實現性到程式萃取——這是「數學基礎的哲學分歧變成軟體工程技術」的直接通道。

證明的兩種「讀法」#

同一個定理「存在 \(x\) 使 \(\phi(x)\) 」可以有兩種證明：

經典證明（例：3.2 節 \(\sqrt2^{\sqrt2}\) 例）： 1. 排中律： \(P \vee \neg P\) 。 2. 兩種情形分別構造。 3. 結論：存在。

構造性證明：直接給出具體的 \(a, b\) 與驗證。

兩者都「證明」了存在，但只有後者可執行。Kreisel 1959 提出著名問題：「非構造性證明中是否藏著可提取的計算內容？」答案：常常有。這一問題開啟了「證明萃取」的整個領域。

可實現性：KLEENE 1945#

定義：對 Heyting 算術的公式 \(\phi\) 與自然數 \(e\) （視為程式碼），遞迴定義「 \(e\) 實現 \(\phi\) 」：

  • \(e\) 實現原子等式 \(s = t\) ⟺ \(s = t\) 真且 \(e = 0\) 。
  • \(e\) 實現 \(\phi \wedge \psi\) ⟺ \(e = \langle e_1, e_2 \rangle\) 且 \(e_1\) 實現 \(\phi\) 、 \(e_2\) 實現 \(\psi\) 。
  • \(e\) 實現 \(\phi \vee \psi\) ⟺ \(e = \langle 0, e_1 \rangle\) 且 \(e_1\) 實現 \(\phi\) ，或 \(e = \langle 1, e_2 \rangle\) 且 \(e_2\) 實現 \(\psi\) （標籤記錄了二擇一）。
  • \(e\) 實現 \(\phi \to \psi\) ⟺ \(e\) 是（的碼）一個全函數，把 \(\phi\) 的每個實現映到 \(\psi\) 的實現。
  • \(e\) 實現 \(\exists x\, \phi(x)\) ⟺ \(e = \langle n, e' \rangle\) 且 \(e'\) 實現 \(\phi(\bar n)\) （見證被記錄）。

可實現性定理： \(HA \vdash \phi \Rightarrow\) 存在 \(e\) 使 \(e\) 實現 \(\phi\) 。

推論（存在性性質）：若 \(HA \vdash \exists x\, \phi(x)\) ，則有具體 \(n\) 使 \(HA \vdash \phi(\bar n)\) ——證明攜帶見證。這正是經典 PA 所沒有的（經典 PA 證 \(\exists x\) 不保證能給出 \(x\) ，如 Goodstein 型情況）。

注意：排中律不可實現——若 \(e\) 實現 \(P \vee \neg P\) ， \(e\) 決定標籤 0 或 1，即 \(e\) 判定 \(P\) ；對不可判定 \(P\) （如停機問題實例），這樣的 \(e\) 不存在（可形式化證明： \(HA + \{P \vee \neg P\}\) 對某些 \(P\) 不可實現一致）。實現性使「哪些經典原則可構造化」變成可判定問題。

證明萃取：從證明到程式#

可實現性的工程化是程式萃取（program extraction）：

  1. 翻譯（Gödel–Gentzen 雙重否定，或 A-翻譯）：經典證明 → 直覺主義證明（可能改變陳述的精確形式）。
  2. 萃取：直覺主義證明 → 演算歸約 → 程式（Curry–Howard：證明項就是程式）。
  3. 驗證：程式的正確性由原證明保證（類型檢查 = 證明檢查）。

歷史地標：

  • Goodman 1970：相對化可實現性——處理 AC 的可實現版本。
  • Gödel 的 Dialectica 解釋（1958）：直覺主義算術到「有限型函數」的翻譯， \(T\) 系統——從證明中提取高階函數。
  • Bates–Constable 的 NuPRL（1980s）：構造性類型論系統，證明即程式，萃取是內建功能。
  • Coq 的兩層設計（1990s）：Prop（命題，可擦除）與 Set（數據，保留計算）——證明的計算內容被顯式管理。

一個具體例子#

例題 9.2.1：對定理「對每個 \(n\) 存在素數 \(p > n\) 」給出構造性證明，並指出其中「可執行」的部分與「規範」的部分。

解：構造：給定 \(n\) ，令 \(N = n! + 1\) （可計算）。 \(N\) 的任何素因子 \(p\) 滿足 \(p > n\) （若 \(p \le n\) 則 \(p \mid n!\) ，故 \(p \nmid n! + 1\) ，矛盾）。而 \(N\) 有素因子（可構造性證明：從 \(N\) 出發枚舉除數找最小素因子——有界搜索，因 \(p \le N\) ）。

可執行部分：計算 \(n! + 1\) ；從 \(2\) 到 \(N\) 枚舉找最小因子（原始遞迴）。 規範部分：「 \(N\) 的最小非平凡因子是素數」——由良序原理（對有限集構造性可用）。

整個證明對應一個原始遞迴程式 \(f(n) = \min\{p : p \mid n!+1,\ p > 1\}\) ，且證明給出 \(f(n) > n\) 的正確性論證。Euclid 的原證明（IX.20，反證法）不給此程式——構造性版本是同一數學事實的可計算化。 \(\blacksquare\)

例題 9.2.2：用 A-翻譯（歸謬翻譯）把經典定理「每個有界單調遞增實數列有上確界」的存在部分轉為構造性版本，並指出需要附加什麼條件。

解：經典陳述在直覺主義中為假（Brouwer 實數可無上確界的可構造逼近）。構造性版本：若 \((a_n)\) 有界遞增且其上界有可計算的模（即存在可計算函數 \(B(\varepsilon)\) 使 \(a_{B(\varepsilon)} > \sup - \varepsilon\) ），則 \(\sup\) 可構造： \(s = \lim\) 由 \(a_{B(2^{-k})}\) 的逼近構造。

A-翻譯的作用：把 \(\neg\neg\exists x\, \phi(x)\) （經典存在）在 \(\phi\) 為「可判定目標」（如 \(|a_m - s| < \varepsilon\) ）時轉為 \(\exists x\) （構造性存在）——翻譯在可判定片段上恢復構造性。這是（Kreisel 的）「非構造證明中的計算內容」的技術核心：經典證明往往隱含著構造，只是需要翻譯來暴露。 \(\blacksquare\)

計算內容的「密度譜」#

證明風格 計算內容 例
純存在（排中律 + 反證） 無或難提取 代數基本定理（經典）
雙重否定翻譯後可構造 可提取（需翻譯） 隱函數定理（經典證明）
直覺主義構造 直接是程式 例題 9.2.1
歸納構造（構造數學） 程式 + 複雜度界 Bishop 的逼近論

經驗事實（Bishop、Richman、Coquand 學派的整理）：數學定理的絕大多數有構造性版本，且構造性證明的程式往往有合理複雜度。非構造性是少數、可翻譯、且常是「定義選擇」問題——這把直覺主義從「全有全無」的哲學變成漸進的工程光譜。

歷史啟示#

  • 證明是「壓縮的計算」：可實現性定理說每個構造性證明編碼一個程式。數學證明與程式的差異是壓縮率與規範性，不是本質。
  • 翻譯是橋樑技術：Gödel–Gentzen、A-翻譯、Dialectica——經典與構造之間有可計算的渡口，兩個世界不是孤島。
  • 存在性質的精確化是邏輯學對軟體的禮物：「證明攜帶見證」（witness property）是形式驗證系統的正確性保證——哲學的分歧（3.2 節）最終變成系統的性質規格。

與其他章節及領域的關聯#

  • 3.2、9.1 節：直覺主義的哲學與邏輯。
  • 6.3 節：翻譯技術在 Hilbert 綱領轉型中的角色。
  • 7.2 節：可實現性把構造性與遞迴函數對齊。
  • 9.3、10.2 節：類型論把「證明即程式」從詮釋升級為同一。
  • 計算機科學：Coq/Agda 的萃取、F* 的反射式驗證；「證明攜帶代碼」（Proof-Carrying Code, Necula 1997）直接以可實現性思想做系統安全。
  • 密碼學：構造性安全證明（歸約給出具體攻擊算法）vs 非構造（存在性歸約）——計算內容的密度影響實際安全。

練習#

  1. 寫出「 \(e\) 實現 \(\forall x\, \phi(x)\) 」的定義，並驗證 \(\forall\) -引入規則保持可實現性。
  2. 對例題 9.2.1 寫出 \(n = 5\) 時程式 \(f\) 的具體執行（ \(5! + 1 = 121 = 11^2\) ， \(f(5) = 11\) ）。
  3. 證明：若 \(HA \vdash \phi \vee \psi\) 則 \(HA \vdash \phi\) 或 \(HA \vdash \psi\) （析取性質，由可實現性）。
  4. 用 A-翻譯處理「每個實數列有收斂子列」的 Bolzano–Weierstrass：指出哪些部分構造、哪些需附加條件。
  5. 思考題：可實現性詮釋下「 \(\neg\neg P \to P\) 不可實現」是否「證明」了直覺主義是對的？比較：這與 3.2 節三學派的哪一種勝利宣言相似，其謬誤為何？

進階研讀：三個深化場景#

場景一：Kreisel 的「無證明即無內容」辯論。Kreisel 1959 反對「非構造證明無內容」的口號，以 A-翻譯展示經典證明的隱含構造。他的格言：「問題不是非構造 vs 構造，而是哪個構造藏在哪個證明裡」——這使「構造性」從立場變成分析任務。

場景二：NuPRL 與計算類型論的工程。Constable 1986 的 NuPRL 系統把 Martin-Löf 類型論（9.3 節）做成互動環境：證明被檢查、程式被萃取、二者同一。直覺主義的「哲學正確」首次變成「軟體可用」——這是 Brouwer 綱領的工程化終點。

場景三：從萃取到機器學習？。神經定理證明（如 AlphaProof）產生形式證明後，證明中的計算內容可被自動萃取為可執行程式——「證明即程式」的 Curry–Howard 原理成為 AI 數學的輸出規範。9.2 節的技術是「數學的可執行化」的理論基座。

名詞速查表#

  • 可實現性：以自然數（程式碼）詮釋構造性證明。
  • 存在性質／析取性質：構造性證明攜帶見證與二擇一標籤。
  • A-翻譯：Kreisel 的歸謬翻譯，在可判定目標上恢復構造性。
  • Dialectica 解釋：Gödel 1958 的高階函數萃取。
  • 程式萃取：從形式證明自動生成可執行程式。
  • Prop／Set 分層：Coq 對「證明可擦除」的管理。

年表速查#

  • 1945：Kleene 可實現性。
  • 1958：Gödel Dialectica。
  • 1959：Kreisel A-翻譯與計算內容問題。
  • 1967：Bishop《分析學基礎》。
  • 1970：Goodman 相對化可實現性。
  • 1980：Bates–Constable NuPRL 計劃。
  • 1986：NuPRL 出版。
  • 1997：Proof-Carrying Code。

深化問答三則#

問：構造性證明「更難寫」嗎？ 答：常見情形相反：構造性證明往往更直接（不需要排中律的分案技巧）。難的部分是重述：經典定理的陳述可能隱含非構造假設（如「有界」的精確含義），構造化需要概念分析。成本在概念澄清，不在證明技巧——這也是構造性數學對概念嚴格化的貢獻。

問：可實現性詮釋是否「唯一正確」的直覺主義語義？ 答：不是，且不應是。可實現性把證明綁定到遞迴函數（7.2 節的特定計算模型）；其他詮釋（Kripke、拓撲、或然論證、HoTT 的同倫詮釋）對應不同的「構造」概念。直覺主義的語義是複數的——這正是它作為「框架」而非「教條」的健康狀態。

問：「證明攜帶見證」對日常數學家有意義嗎？ 答：有兩種意義：其一，寫作時知道自己的存在證明是否「可執行」（自我檢查）；其二，形式驗證時知道定理的使用者可以提取算法（如 Lean 數學庫中「存在性定理」的計算可用性標注）。見證性質把「數學的用」與「數學的證」連成一體——這是 20 世紀基礎辯論給 21 世紀數學實踐的具體饋贈。

（本節完）