Let's play Agda 
{-# OPTIONS --cubical-compatible #-}
module Padova2025-zh-TW.ComputationalContent.Intro where

簡介#

建構性與非建構性證明#

是否存在無理數 x 與 y，使得它們的冪 xy 是有理數？為了回顧並固定定義：一個實數稱為有理數，若且唯若它可以寫成 a/b 的形式，其中 a 與 b 為整數。（這等價於該數具有循環的小數展開，例如 1/3 = 0.333…）一個數稱為無理數，若且唯若它不是有理數（例如 √2）。

根據下面的證明，答案是是：

定理。 存在無理數 x 與 y 使得 xy 是有理數。

證明。 √2√2 要嘛是有理數，要嘛不是。在第一種情況下，我們可以取 x = √2 且 y = √2。 在第二種情況下，我們可以取 x = √2√2 且 y = √2；確實，此時 xy = √2√2 · √2 = √2² = 2 是有理數。∎

這就解決了「是否存在冪為有理數的無理數」這個問題。然而，對於所展示的證明，可能仍殘留一種揮之不去的不滿： 只要我們不知道這兩種情況中哪一種成立，就無法指著任何一個特定的例子，說它是這樣的一對數。

有沒有資訊量更豐富的證明？讓我們再試一次：

定理。 存在無理數 x 與 y 使得 xy 是有理數。

證明。 取 x = √2 且 y = log√2(3)。那麼眾所周知 x 是無理數；y 的無理性或許較不為人所知， 但實際上比 √2 的無理性更容易建立；而 xy = 3 是有理數。∎

第二個證明是建構性的，明確地為存在命題提供了見證。相對地，第一個證明確立了命題為真，卻沒有揭露任何見證， 這樣的證明被稱為非建構性的。這類證明在古典數學（數學的標準風格）中被接受；在另一種風格的建構性數學中則不被接受。

建構性數學的獨特之處#

在建構性數學中，我們接受古典數學幾乎所有的公理與推論規則，但我們不使用排中律（A ∨ ¬ A），不使用與之 （等價的）雙重否定消去律 （¬¬ A ⇒ A），也不使用選擇公理。但另一方面，我們也不公設它們的否定：相反地， 我們對這些原理保持中立的不可知論立場。因此，每個建構性證明也都是有效的古典證明。（令人驚奇的是， 某種特定意義下的逆命題也成立，只是不是字面上的意思。）

建構性數學有幾個獨特的特色：

  • 建構性證明資訊量更豐富。例如，在建構性數學中，我們不被允許僅僅透過驗證「方程式不可能沒有解」來確立方程式有解。 相反地，存在性的建構性證明必須提供見證，也就是一對東西：一個值，以及該值確實是方程式的解的見證。

  • 建構性數學讓我們能做出更細緻的區分，例如在集合是有居民的（意思是它包含一個元素）與集合僅僅不是空的 （意思是假設它是空的會蘊涵矛盾）之間，或者更一般地，在一個陳述與它的雙重否定之間。 這些更細緻的區分，又帶來演算法與幾何上的後果。

  • 每個建構性結果都有演算法詮釋——每個建構性證明都可以當成電腦程式來執行。例如：每個關於方程式有解的建構性存在性證明， 都可以當成演算法來執行，算出這樣的解。由於 Agda 預設是建構性的系統，我們已經多次觀察到邏輯與可計算性之間的這種連結。

  • 每個建構性結果都有適用於連續族的幾何詮釋。例如，建構性分析的一個定理說，每個取值有負有正的嚴格單調函數 ℝ → ℝ 都有零點。 藉由建構性證明的幾何詮釋，我們可以立刻推出：在每個由取值有負有正的嚴格單調函數構成的連續族中，它們的零點可以局部地以連續的方式選取。 （一個更複雜的例子，是建構性線性代數的定理：每個有限生成的向量空間並非沒有基底。藉由幾何詮釋，我們可以立刻推出： 約化概形（reduced scheme）上每個有限型的層，在一個稠密開集上局部是有限自由的， 這就是代數幾何中的 Grothendieck 一般自由性引理（generic freeness lemma）。）

  • 建構性數學與一些有趣但反古典的公理相容，例如「每個函數 ℝ → ℝ 都是連續的」或「每個函數 ℕ → ℕ 都是可計算的」。

希爾伯特失敗的計畫令人驚訝的成功#

古典數學的每個結果都能被建構化嗎？照字面來看，這個問題有明確的否定答案。已知許多結果只有古典證明，因為它們蘊涵了非建構性的原理：

  • 在 Zermelo–Fraenkel 集合論之上，「每個向量空間都有基底」這個陳述蘊涵選擇公理。
  • 在 Zermelo–Fraenkel 集合論之上，「每個交換環都有極大理想」這個陳述蘊涵選擇公理。
  • 在直覺主義 Zermelo–Fraenkel 集合論之上，「每個有居民的自然數集合都包含一個最小元素」這個陳述蘊涵排中律。

但這些觀察只是一個更宏大故事的開端。希爾伯特區分了抽象結果——通常屬於基礎建設性質——與具體結果， 後者涉及更具體的數學對象，例如自然數。許多抽象結果無法建構性地證明，但它們的具體推論往往可以。

  • 「每個函數 ℕ → ℕ 都有最小值」這個結果在建構性數學中不可用，但它的推論 Dickson 引理卻可用。
  • 無窮鴿籠原理（說每個無窮的二元序列都包含無限多個 false 項或無限多個 true 項）在建構性數學中不可用， 但它的推論有限鴿籠原理卻可用。
  • 「每個交換環都有極大理想」這個結果在建構性數學中不可用，但關於矩陣的推論卻可用：例如，我們確實能建構性地得到， 只有在零環上，列數多於行數的矩陣才可能是滿射。

古典證明在許多情況下可以被「開採」出建構性、因而是計算上的內容；因此，古典證明可以視為資訊量更豐富的建構性證明的藍圖。 在許多情況下，甚至有形式的後設定理支持這個哲學，保證這項萃取工作的可行性。在這個精煉的意義下，希爾伯特的計畫已經大獲成功， 而只能藉由超限手段取得的輔助對象，例如無窮序列的最小值或極大理想，可以被視為方便的虛構：嚴格說來， 它們在建構性數學中並不可用，但它們不妨就當作可用，因為它們的推論是可用的。

接下來的模組專門研究一種特別多用途的建構化技術，它基於雙重否定單子。這個方法可用來從古典證明中消去排中律的應用。 （至於消去選擇公理的應用，則使用其他技術，通常基於形式拓撲或拓撲斯理論。）