碼上快樂

相關內容    簡體    繁體

談談數學里的構造主義（constructivism）、直覺主義（intuitionism）和數學基礎

本文轉載自   查看原文   2021-07-29 13:10   328    科學

https://zhuanlan.zhihu.com/p/22389755

翻開數學史的書籍，構造主義仿佛是二十世紀初期的一股叛逆思潮。它曾經很酷，但是卻缺乏主流數學家的關注，甚至遭到批判。本文試圖梳理一下構造主義的脈絡，始於構造主義，終於 univalence axiom (i.e. homotopy type theory).

§-1. 構造主義和直覺主義

用過分簡單的話講，構造主義的核心就是 “要證明一個東西存在，必須把它構造出來”。這直接否定了人們熟悉的反證法。把反證法拿走，后果有多嚴重呢？

從某些層面上講，它並沒有人們想象的那么嚴重——只要澄清了一些概念並且做一些仔細地重新敘述，有些用反證法證明的命題其實並不需要反證法：比如歐幾里得仔細選取的對 “素數有無窮個” 這個命題的陳述，本質上說的是

任意一個有限集合到素數的集合都存在一個單射。

完全避開了 “無窮” 的概念這一蹚渾水。（從歐幾里得對平面幾何第五公理的謹慎態度也可以理解，他絕對不會用 “素數有無窮個” 這種描述。）

“[公式]是無理數” 這個命題，也可以轉化為

對任意的自然數 [公式], 我們有 [公式]或者 [公式].

並且可以構造性地證明（證明比一般的用反證法證明稍微冗長些）。

在另一些層面上，構造主義帶來的困難則大得多——構造主義的一支，布勞威爾（L. E. J. Brouwer）的直覺主義直接要求 "there exists" 被解讀為 'there can be constructed', 也就是說 'we can compute'. 這直接導致了了以下的 “神邏輯”:

[公式]對於數列 [公式], 即使 “ [公式]（對任意的 [公式]）” 這一命題不成立，我們也不能得出 [公式]（“存在”  [公式]使得 [公式]）

因為——雖然在非直覺主義的意義下有這么一個[公式], 但是這個[公式]並不是被構造出來的。沒有 “算法” 告訴你怎么計算出這個[公式]

不能構造出來就不存在？沒錯，布勞威爾就像蘋果公司一樣，再一次定義了 “存在”！

§0. 如何解讀神邏輯

要理解這個神邏輯，不能拘泥於 “存在” 這兩個字在自然語言中的字面意思，而是把 “[公式]” 這個量詞 (quantifier) 看做一個純粹的符號，再接受布勞威爾對這個詞的解讀——換句話講建構在直覺主義上的數學和邏輯，其實是我們熟悉的那套東西的一個兄弟，只是 “[公式]” 這個基因發生了一點變異。

由於 “[公式]” 的變異，直覺主義的數學發展相比遲緩。因為，[公式]直接否定了數學中一個常用的邏輯命題——排中律！排中律的陳述很簡單：

對於任意的命題 [公式],  [公式]成立。（也就是說， [公式]或非 [公式]總有一個成立。）

加上量詞的版本更能體現排中律和[公式]的不可調和之處——加上量詞的排中律是這樣的：

[公式].

用直覺主義的方式來闡釋 “[公式]”, 顯然無法接受排中律——即使我們否定了 “對任意的[公式], 都有[公式]” 這一命題，我們也不能算出一個使得[公式]不成立的[公式].

把排中律抽走，對直覺主義的數學影響有多大呢？很大：

（注：這里原文有誤，已修改）由 Diaconescu's theorem 排中律是選擇公理的推論，抽走排中律，選擇公理也不能成立，這就抽走了很多現代數學里最重要的引理，動搖了很多比較現代的理論的基石——

  1. 分析上，沒有排中律，不能得出[公式]（即使知道[公式]不成立也不能推出[公式]的絕對值大於[公式].）類似地，也沒有中值定理。
  2. 代數上，沒有選擇公理，甚至不能證明任意一個環的存在極大理想！

這種限制對於很多數學家而言是萬萬不能接受的。實際上，沒有排中律的話，甚至不能說一個實數要么是有理數，要么是無理數！（提示，設[公式]是一個取值在[公式]中的遞減數列，考慮[公式]的有理性和前面的神邏輯[公式]的關系）

 

§1. 一個有趣的觀點

實際上，高中或者大學的某些數學之所以對一部分人困難，就是因為我們就放棄了構造主義！

首先，高中的數學和初中是很不一樣的——並不是說初中研究了線性函數和二次函數，高中就研究三次四次函數，大學再研究五次六次函數。回頭看來，兩者最大的區別是，用的數學基礎發生了重大變化——初中的數學，無所謂基礎，所有的研究對象都是實數軸上的一次或者二次函數，所有的函數都可以在計算器上摁出來，其實在學生腦子里默默建構了構造主義的習慣。而高中開始，數學就慢慢地建立在集合論的基礎上了。

集合論帶來的，是非構造性。兩個集合之間的映射，定義起來並不平凡：

給定集合 [公式], 他們之間的一個映射是一個關系，對於任意的 [公式], 有唯一的 [公式], 這個關系記作  [公式].

換句話講，[公式]對應的是[公式]的一個滿足如下條件的子集[公式]

[公式]（存在唯一的 [公式]）使得  [公式]

真正理解這個定義的人，難免痛恨 “一個映射/函數就是一個公式” 的常見誤解（鄙人就曾經是痛恨者中的一員）。回過頭來看，這種誤解其實代表着構造主義和集合論的沖突。按照集合論的定義，實數軸上的實值函數，其實是[公式]的一類的子集，對每個[公式] “分配” 了一個值[公式]——有沒有讓人窺見選擇公理的影子？大多數這樣的函數，都是 “不可計算” 的。

 

就是這一點點非構造主義，以奇怪的形式把很多人絆倒在構造在集合論基礎上的現代數學的門檻上。門檻本身在哪里並不重要——可能在集合論，也可能在數學分析，或者實變函數論，但歸根結底都是那一點點非構造主義。

類似的例子還有抽象代數。很多人在初次學習的時候本能地拒絕 “一個群是一個集合加上一個滿足某些條件的二元運算” 這樣的抽象定義，但是能接受矩陣群的概念，本質上也是非構造主義在作祟。用面向對象編程的語言來說，矩陣和一個抽象的集合的元素的區別在於，矩陣群自帶元素的 constructor 和 methods. 但是用抽象的集合給出的群，就好像只帶着 virtual methods 的 object, 會被一些人腦子里的編譯器拒絕。

§2. 集合論與計算機，一個小故事

實際上，集合論以及上述的非構造主義，不光把一部分學生攔在了現代數學的門檻之外，還攔住了一個重要的角色——計算機。

這個 “攔住” 是實質性的：不是說囿於計算性能的門檻，計算機雖說可以理解集合論，但無法用於實際用途。而是由於某些原因，多數數學家接受的作為數學基礎的 ZFC 集合論，實在無法讓計算機接受。

實際上，在集合論的框架下，多數數學家也沒辦法從純粹集合論的角度思考數學——比如實數的概念，只有在最嚴格的分析中才視作有理數的柯西序列的等價類，平時腦子里想象的都是實數軸上的點。數學基礎和實踐的這種巨大差異，才是計算機的最大絆腳石。

就算有辦法把以 ZFC 集合論為基礎的內容硬塞給計算機，其實還有下面這種風險：假設某一天計算機利用強大的計算能力，用純粹的邏輯找到了黎曼猜想的證明，但人類仔細閱讀計算機給出的證明的時候，發現在關鍵的一步，計算機說

因為  [公式], 所以...

等等，[公式] 是什么鬼？！計算機辯解道，根據定義，萬物都是集合，首先有空集[公式], 然后通過 [公式] 來定義自然數[公式]嘛。人類數學家急了，這只是自然數的集合論模型之一啊！[公式] 這種依賴於模型的東西，怎么能用來證明這么重要的定理呢？這時候，另一台計算機，用另一個自然數的集合論模型，也找到了一個黎曼猜想的證明，但是這台計算機里，自然數的模型[公式]是通過[公式]來定義的。而在證明的關鍵一步，它用到了 [公式]... 我們甚至沒法比較兩台計算機給出的證明是否相同。

 

在人類看來，兩個自然數的模型的選取，本來是無關緊要的東西，不管怎么說，任意兩個模型都是同構的嘛。對重要命題的證明不應該依賴於模型的選取，這就好像對一個關於整數的結論的證明不應該依賴於整數的十進制表示一樣顯然。同構的話，對一個成立的命題，可以通過同構 “搬” 到另一個上，但顯然，“可以搬動的性質” 並不包括[公式]這種奇怪的東西——這又是一個沒法跟計算機解釋的怪現象。

§3. 從集合論到類型論 (type theory)

花開兩朵，各表一枝。七十年代末，瑞典人 Martin-Löf 做出了一個重要的發現，即 algorithmic mathematics, 也就是計算機科學, 等價於只用直覺主義邏輯的數學。在 Martin-Löf 發展的構造性類型理論 (constructive type theory) 中，有以下的對應關系

 

熟悉集合論的讀者應該能注意到上述表格的第一行的不尋常之處——在 Martin-Löf type theory 中，一個 “函數” 就是一個 “公式”！（只不過這個公式可以稍微復雜一點，寫成一段代碼或者算法而已。）這套觀點完全丟棄了原來對函數的定義，[公式]的函數不再是[公式]的一個特殊子集，而是從一個類型[公式] 的輸入到一個類型[公式]的輸出的一個計算的步驟 (procedure) !

實際上，盡管離學術界廣泛接受還有一定距離，type theory 其實很有適用於數學基礎的潛力，並且是一個從誕生之初就適合計算機理解的數學基礎。

在類型論中，“集合” 的概念被 “類型” (type) 取代，自然數、整數、有理數，都有對應的類型。乍一看這和集合論 “萬物都是集合” 沒啥不同，只是把 “放在一起的一堆東西” 的名字從集合 (set) 改成了類型 (type), 並且把記號[公式] 改成了[公式]. 實際上，兩者差了十萬八千里——在集合論中，我們可以構造一個集合[公式], 和另一個集合[公式]（兩者都是從空集[公式]出發，用 ZFC 集合論允許的運算進行構造得到的結果，比如[公式]），再討論

[公式]是否成立？

這樣的問題。而在 type theory（intensional type theory, 下同）中，沒有辦法 “給出” 一個不 “屬於” 任何類型的[公式], 再去討論它和別的類型有沒有從屬關系，只能一次性地給出判定[公式]——注意這里的用詞，[公式]是一個判定 (judgement)，而不是一個取值有可能真也有可能假的命題，一個判定從擺上紙面的那一刻就自動成立。在集合論中，如果[公式], [公式]是一個滿足[公式]的集合，則我們也有[公式]. 類似的話在 type theory 中毫無意義。——實際上，type theory 的這種討論方式，反倒更接近現代數學實踐，因為沒有人會真的拿兩個不相干的東西[公式]再問 “[公式]是否成立”，而通常是 “設[公式]是拓撲空間，[公式]是[公式]中的一個點”，從這個角度上說，這種做法更接近於給出判定[公式].

更有趣的一點是，類型論的法則自動地包含了基本的邏輯！一個命題，在類型論中可以寫成一個類型[公式], 其證明則是構造那個類型中的一項 (term) [公式]. 命題[公式]則變成了一個新的 type [公式], 其 “證明” 則是在類型論的意義下構造[公式]到[公式]的一個函數。對照之下，數理邏輯獨立於集合論而存在。

集合論中最基本的 “命題”，[公式] 在 type theory 中已經不能討論。另一類命題，即對於[公式]是否有[公式], 則在 type theory 中有深遠的推廣。前面說了，任意一個命題，都有自己的類型, [公式] 這樣的，也不例外——它對應的類型，叫 identity type, 記做[公式]. 相比之下，集合論中的命題，無非是兩個元素的一個比較，相等，則[公式]只是同一對象的兩個符號而已，可以互相置換（substitution, 等量代換是中學數學中最基本的操作）；不相等，則他們之間在集合論的意義下沒有任何聯系。[公式] 是個 type 這件事情，不僅僅是個記號，意味着 type theory 的任何構造，都可以對它進行。

§4. 尾聲：從 Extensionality 到 Univalence

兩個集合什么時候相等呢？在 ZFC 集合論中，這是由一條叫做外延性 (extensionality) 的公理保證的：[公式]. 也就是說，如果兩個集合包含的元素一模一樣，我們就說兩個集合相等。

這個公理完全不能用在 type theory 中——根本沒有[公式]這個說法，要給出[公式], 必須以[公式]這樣的方式，這時候[公式]就成了徹底的偽命題，沒法討論。

但是，在類型論中討論兩個類型的 equality, 還是有一定意義：實際上，任意兩個 type [公式] 都是一個更大的 type, 即 universe [公式] 中的項，所以給出兩個類型其實是給定了[公式], 我們當然可以定義 identity type [公式], 但是，怎么描述這個類型呢？

Voevodsky 在 2009 年給出了一個誘人的答案，即 univalence axiom.

從[公式]這個類型到[公式]這個類型，有個 map. 對於任意一個[公式], 我們都能得到一個[公式]，這個[公式]有個特殊的性質，它（together with other data）實際上構成了[公式]到[公式]的一個 equivalence. ——熟悉范疇論的讀者應該不會覺得奇怪。

Equivalence 的定義在這里恕不展開了，只能說任給[公式]，可以定義 type of equivalences[公式]. 用不嚴格的符號說，前述的 map[公式]實際上給出了 identity type 到 type of equivalences 的一個 map. Voevodsky 引入的 univalence 公理說，這個 map 是一個 equivalence.

 

引入 univalence 公理相當於把終極的外延性 (extensionality) 引入了 type theory。說到底，extensionality 是關於什么時候能判定兩個結構在某種意義下 “相同” 的公理，對於集合來說，這是很簡單的。但是在通常的數學中，有些熟悉例子，兩個很一致的東西（即關鍵的性質可以像前面說的那樣 “搬來搬去” (transport)），不能說他們相等。比如任意兩個[公式]維線性空間，我們只能說他們 “同構” 而不能說他們相等，因為有太多種方式把他們等同起來（選取基以后任意的[公式]可逆矩陣都給出同構）；對於兩個范疇，甚至只能說他們 “等價” 而不能說他們同構（因為在集合層面並不是一一對應）。這些褶皺，都能用 univalence axiom 一一撫平。

更體現 univalence axiom 威力的地方在於，有了 univalence axiom, 能很好地對任意的自然數[公式]定義[公式]（[公式]）——定義 [公式] 或者[公式]其實是很有意義的，也很困難（比如通常的 algebraic stacks 也就是[公式]的情形而已）。Grothendieck 在 Esquisse d'un Programme (Sketch of a Programme) 的第七節 Pursuing Stacks 描繪了用 homotopic algebra 來定義 [公式]的可能性。Univalence axiom 可以看做對 Grothendieck 描繪的藍圖的一個回應。

 

§5. 注釋

  1. 用 “瑞典人” 來描述 Martin-Löf 的主要原因是他太神，沒法用 “數學家” 這樣的詞簡單概括，引用 Wikipedia 第一句做個注解：Per Erik Rutger Martin-Löf (born May 8, 1942) is a Swedish logician, philosopher, and mathematical statistician.（邏輯學家，哲學家和數理統計學家）
  2. Type theory 其實最早是羅素提出來的。這里介紹的是 Martin-Löf type theory. Martin-Löf 發展的 type theory 其實有好幾個版本, 參見 Intuitionistic type theory#Martin-Löf_Type_Theories. 我認為 identity type 是最大的創新之一。
  3. 計算機證明黎曼猜想和自然數的定義那個故事是編的，但是很有必要定義一種數學基礎使得所有的命題都可以 “搬來搬去”，則是一種共識。“It should be impossible to formulate a statement which is not invariant with respect to equivalences.” ——T. Coquand
  4. 讓計算機理解集合論並沒有文中說的那么困難，參見 Mizar system —— A proof assistant based on first-order logic, in a natural deduction style, and Tarski–Grothendieck set theory. (Tarski-Grothendieck set theory 是 ZFC 的一個 non-conservertive extension, 添加了 Tarski 公理: 對任意一個集合[公式]存在一個 Grothendieck universe[公式]使得[公式].)
  5. 可能有讀者會問 type theory 里這套 Programming 和 Mathematics 的對應和所謂的 Curry-Howard Isomorphism 有什么區別和聯系, 實際上上述對應相當於把 Curry-Howard isomorphism 擴展到了 dependent type theory. 相當於 Curry–Howard isomorphism 加上了謂詞邏輯的的強化版。
  6. 集合論的 extensionality 公理的推論之一是，對於兩個集合之間的函數[公式], [公式]： 因為作為[公式]的子集，[公式]的圖像[公式]在函數值完全相當的時候完全重合，所以作為集合相等。
  7. 用不嚴謹的話講，加入了 univalence axiom 的 type theory, 叫 homotopy type theory. 我故意在正文里避開了這個詞。
  8. Jacob Lurie 以集合論為基礎來定義[公式], 做了很重要的工作，但他的工作與 homotopy type theory 無關。竊認為 Jacob Lurie 工作的困難程度可以反過來說明 homotopy type theory 的重要性。

 

§6. 參考

  1. 關於構造主義的一個比較耐讀的參考 (40 pp.): Constructive Mathematics in Theory and Programming Practice, Douglas BRIDGES and Steve REEVES
  2. Constructive Mathematics (Stanford Encyclopedia of Philosophy)
  3. 有一定數學背景，且對 Homotopy type theory 有興趣的讀者很有必要看看這三個 slides:

 

（題圖：Wikipedia File:Logic.svg）


免責聲明！

本站轉載的文章為個人學習借鑒使用，本站對版權不負任何法律責任。如果侵犯了您的隱私權益，請聯系本站郵箱yoyou2525@163.com刪除。



猜您在找 再談談數學 數學里的e到底指什么 追蹤子彈-初中簡單的物理和數學 遞歸和數學歸納法 談談php里的DAO Model AR 數學基礎之微積分 基礎數學知識 談談Python中列表、元組和數組的區別和騷操作 Java里的構造函數(構造方法) 傅里葉級數的數學推導
 
粵ICP備18138465號   © 2018-2025 CODEPRJ.COM