{-# OPTIONS --cubical-compatible #-}
module Padova2025-zh-TW.Explorations.Forcing.Intro where

簡介#

在代數與分析中，我們習慣把給定的數學結構擴大成更適合某些任務的較大結構。例如，序列

3, 3.1, 3.14, 3.141, …

以及許多其他序列在 ℚ 中都不收斂，因此我們把 ℚ 擴大為 ℝ。或者，體 ℝ 不含 -1 的平方根，因此我們把 ℝ 擴大為 ℂ。

1970 年代，Paul Cohen 開創了一項技術，它擴大的不是某個特定的數學結構（例如體或環），而是給定的數學宇宙本身。 例如，從基礎宇宙出發，我們可以建構所謂的 強迫擴張（forcing extensions），其中……

• 存在一個大小介於 ℕ 與 ℝ 之間的集合（「Cohen 強迫法」），
• 基礎宇宙中某個給定的不可數集合 X 現在變得可數（「Lévy 塌縮」），或
• 存在一個「隨機實數」（「隨機強迫法」）。

強迫法成為探索集合論可能性範圍的無價工具——這個範圍相當大，因為 Zermelo–Fraenkel 集合論的公理對「集合」這個概念嚴重地欠規定 （即使加上選擇公理也一樣）。

在建構性數學中的應用#

強迫法的效用也受到建構性數學社群的認可，通常以 Grothendieck 拓撲斯的面貌出現，它在那裡幫助我們從古典證明中萃取計算內容。

例如，給定帶單位元的交換環 R，我們可以 擴大宇宙來找到一個極大理想，從而避免使用 Zorn 引理 （Zorn 引理會在基礎宇宙中就憑空造出一個極大理想，但它在建構性數學中不可用）。

或者，我們可以擴大宇宙，使其包含所謂的泛型 R-代數（generic algebra），這是合成代數幾何的起點。 這種代數幾何的處理方式，讓我們可以用一種簡單的語言做現代 Grothendieck 風格的代數幾何（在任意的基概形上）， 這種語言讓人想起古典義大利代數幾何學派（不過他們只在 ℂ 上工作），並且避免了處理概形的技術細節。

從下方逼近#

強迫法的關鍵想法，是用基礎宇宙中適當的（通常是有限的）集合來逼近所要的新集合，就像我們用上面顯示的有理數來逼近 π 一樣。

例如，我們可以用有限生成的理想 a 來逼近給定交換環 R 中一個（幻想的）素理想，從 a = (0) 開始。 當我們遇到 xy ∈ a 的情況時，需要把近似 a 改進為 a + (x) 或 a + (y)，以確保在極限中滿足素理想條件 xy ∈ p ⇒ (x ∈ p ∨ y ∈ p)。

令人驚奇的是，即使在古典數學證明極限不存在的情況下，這個想法依然有效。例如，設 X 是一個有居民的不可數集合，比如 ℝ。 那麼依定義，不存在滿射 ℕ ↠ X。但我們可以用 X 的元素所成的有限串列來逼近一個虛構的這種滿射：例如， 我們可以把有限串列 a ∷ b ∷ c ∷ [] 視為部分定義、勉強稱得上滿射的函數 f，其中 f(0) = a、f(1) = b、f(2) = c。 隨著時間推移，這個近似可以演變成形如 a ∷ b ∷ c ∷ x ∷ [] 的串列，其中 x 遍歷 X 的元素，使 f 定義得更完整； 或者演變成形如 a ∷ b ∷ c ∷ xs 的串列，其中 xs 遍歷 X 的元素所成的有限串列，使得新的近似把給定的元素 w 當作其中一項，讓 f 變得更接近滿射。

要在 Agda 中精確地描述強迫法，並在所有細節上忠實於黑板數學中對 Grothendieck 拓撲斯的通常表述，是一項挑戰。 在接下來的幾節中，我們會探索一個簡化的版本，它有某些問題，但仍讓我們能把玩這一圈想法（並成功陳述與證明有啟發性的結果）。