維基百科

泛等基礎

泛等基礎是一種建立數學基礎的方法，它以類型作為構建數學結構的基礎對象。泛等基礎中的類型並不完全對應於集合論基礎中的任何東西，但它們都可以視作一個空間，其中相等類型對應於同倫等價空間，類型的相等元素對應於由路徑（Path）連接的空間上的點。泛等基礎啟發自早期的Hermann Grassmann和Georg Cantor的數學哲學理念，以及Alexander Grothendieck風格的「範疇論」式數學。泛等基礎脫胎自（且兼容於）經典的一階邏輯，並使用Martin-Löf類型論的一個版本代替它作為形式化演繹推理系統的底層基礎。泛等基礎的發展與同倫類型論的發展密切相關。

泛等基礎與結構主義兼容，因此沿用了數學結構（如範疇論）中合適的記法[1]。

歷史

編輯

泛等基礎的主要理念是由Vladimir Voevodsky在2006年至2009年期間提出的。泛等基礎和早期思想之間的哲學聯繫的唯一參考來源是 Voevodsky在2014年 Bernays 的講座[2]。「泛等性（Univalence）」這個名字是由 Voevodsky 提出的[3][4]。有關泛等基礎現階段思想的貢獻歷史的詳細討論可以在同倫類型理論（HoTT）頁面找到。

泛等基礎的一個基本特徵是，當它與 Martin-Löf 類型論（MLTT）相結合時，為現代數學的形式化提供了一個實用的系統。使用該系統和現代證明助手（例如Coq和Agda）已經形式化了相當多的數學。第一個此類庫名為「Foundations」，由 Vladimir Voevodsky 於2010年創建[5]。現在 Foundations 是一個由多位作者共同開發的名為UniMath的更大開發項目的一部分[6]。基金會還啟發了其他形式化數學庫，例如 HoTT Coq 庫[7]和 HoTT Agda 庫[8]，它們在新的方向上發展了泛等性的理念。

泛等基礎的一個重要里程碑是2014年6月由Thierry Coquand主持的Bourbaki 研討會演講[9]。

主要概念

編輯

泛等基礎源於某些基於高階範疇論建立數學基礎的嘗試。最接近泛等基礎的早期思想是Michael Makkai表示「具有依值種類（Dependent Sorts）的一階邏輯」（FOLDS）的思想[10]。泛等基礎和 Makkai 預想的基礎之間的主要區別是認識到「集合的高維類比」對應於無窮廣群，並且範疇應被視為偏序集的高維類比。

最初，泛等基礎是由 Vladimir Voevodsky 設計的，目的是使那些從事經典純數學工作的人能夠使用計算機來驗證他們的定理和構造。泛等基礎本質上是構造性的這一事實是在編寫 Foundations 庫（現在是 UniMath 的一部分）的過程中發現的。目前，在泛等基礎上，經典數學被認為是構造性數學的一個「收縮」，即經典數學既是由使用排中律作為假設的定理和構造組成的構造性數學的一個子集，又是構造性數學乘以等價關係再對排中律公理取模的「商」。

在基於 Martin-Löf 類型理論及其衍生理論（例如歸納構造演算）的泛等基礎形式化系統中，集合的高維類比由類型表示。類型的集合通過h-層級（或同倫層級）的概念進行分層[11]。

h-層級0的類型是等於一個點的類型。它們也稱為可收縮類型。

h-層級1的類型是任意兩個元素相等的類型。這樣的類型在泛等基礎中叫做「命題」[11]。 h-層級中命題的定義與早期 Awodey 和 Bauer 提出的定義一致[12]。因此，雖然所有命題都是類型，但並非所有類型都是命題。具有「需要證明」這一性質的類型才能成為命題。例如，泛等基礎中的第一個基本構造叫做 iscontr，它是一個從類型到類型的函數。如果 X 是一個類型，則 iscontr X 是一個具有對象的類型若且唯若 X 是可收縮的。這是一個定理（在 UniMath 庫中稱為 isapropiscontr）：對於任何 X ，類型 iscontr X 具有 h-層級1，因此可收縮類型是一種性質。 h-層級1類型的對象所擁有的屬性與高階 h-層級類型的對象所擁有的結構之間的這種區別在泛等基礎中非常重要。

h-層級2的類型稱為集合[11]。自然數的類型具有h-層級2是一個定理（在 UniMath 中稱為 isasetnat）。泛等基礎的創造者聲稱，Martin-Löf 類型理論中集合的泛等形式化是目前對集合論數學（無論是構造性的還是經典的）所有方面進行形式推理的最佳環境[13]。

範疇被定義為（參見 UniMath 中的 RezkCompletion 庫）h-層級3的類型，並帶有一個附加結構，該結構與定義偏序集的 h-層級2類型的結構非常相似。泛等基礎中的範疇論與集合論世界中的範疇論有些不同，也更豐富，其中最關鍵的區別就是是預範疇和範疇之間的區別[14]。

關於泛等基礎的主要思想及其與構造性數學的聯繫參見 Thierry Coquand 的教程[a]。從經典數學角度對主要思想的介紹參見 Alvaro Pelayo 和 Michael Warren 在2014年的綜述[17]，以及 Daniel Grayson 的介紹[18]。另請參閱：Vladimir Voevodsky（2014）。 [19]

目前的進展

編輯

Chris Kapulkin、Peter LeFanu Lumsdaine 和 Vladimir Voevodsky 撰寫的論文中可以找到 Voevodsky 構造具有 Kan-單純集的 Martin-Löf 類型論的泛等模型的說明[20]。Michael Shulman構造了具有單純集逆圖範疇中值的泛等模型[21]。這些模型表明，泛等公理獨立於命題的排中律公理。

Voevodsky 的模型被認為是非構造性的，因為它以不可消除的方式使用選擇公理。

為 Martin-Löf 類型理論的規則找到一個構造性解釋，同時滿足泛等公理[b]和自然數規範性的問題仍是個開放問題。Marc Bezem、Thierry Coquand和Simon Huber[23]的論文中概述了部分解決方案，剩下的關鍵問題是恆同類型消除子的可計算性。這篇論文的思想現在正在幾個方向上發展，包括立方型理論的發展[24]。

新的方向

編輯

大多數在泛等基礎框架內的數學形式化工作都是使用歸納構造演算（CIC）的各種子系統和擴展來完成的。

儘管進行了多次嘗試，但仍無法使用 CIC 構造三個常規問題的解決方案：

  1. 使用類型定義半單純形類型、H-類型或(∞,1)-範疇結構。
  2. 使用全域管理系統來擴展 CIC，使其能實現尺寸調整規則。
  3. 開發泛等公理的構造性變體[25]。

這些未解決的問題表明，雖然 CIC 對於泛等基礎發展的初始階段來說是一個很好的系統，但在更複雜方面的工作中轉向使用計算機證明助手將需要開發新一代的形式演繹和計算系統。

另見

編輯

註記

編輯
  1. ^ Awodey, Steve. Structuralism, Invariance, and Univalence (PDF). Philosophia Mathematica. 2014, 22 (1): 1–11. CiteSeerX 10.1.1.691.8113  . doi:10.1093/philmat/nkt030. 
  2. ^ Voevodsky, Vladimir. Foundations of mathematics — their past, present and future. The 2014 Paul Bernays Lectures (ETH Zurich). September 9–10, 2014.  See item 11 at Voevodsky Lectures
  3. ^ univalence axiom in nLab
  4. ^ Martín Hötzel Escardó (October 18, 2018) A self-contained, brief and complete formulation of Voevodsky’s Univalence Axiom
  5. ^ Foundations library, see https://github.com/vladimirias/Foundations
  6. ^ UniMath library, see https://github.com/UniMath/UniMath
  7. ^ HoTT Coq library, see https://github.com/HoTT/HoTT
  8. ^ HoTT Agda library, see https://github.com/HoTT/HoTT-Agda
  9. ^ Coquand's Bourbaki Lecture Paper and Video
  10. ^ Makkai, M. First Order Logic with Dependent Sorts, with Applications to Category Theory (PDF). FOLDS. 1995. 
  11. ^ 11.0 11.1 11.2 See Pelayo & Warren 2014
  12. ^ Awodey, Steven; Bauer, Andrej. Propositions as [types] . J. Log. Comput. 2004, 14 (4): 447–471. doi:10.1093/logcom/14.4.447. 
  13. ^ Voevodsky 2014
  14. ^ See Ahrens, Benedikt; Kapulkin, Chris; Shulman, Michael. Univalent categories and the Rezk completion. Mathematical Structures in Computer Science. 2015, 25 (5): 1010–1039. S2CID 1135785. arXiv:1303.0584  . doi:10.1017/S0960129514000486. 
  15. ^ Coquand (2014) part 1
  16. ^ Coquand (2014) part 2
  17. ^ Pelayo, Álvaro; Warren, Michael A. Homotopy type theory and Voevodsky's univalent foundations. Bulletin of the American Mathematical Society. 2014, 51 (4): 597–648. arXiv:1210.5658  . doi:10.1090/S0273-0979-2014-01456-9  . 
  18. ^ Grayson, Daniel R. An introduction to univalent foundations for mathematicians. Bulletin of the American Mathematical Society. 2018, 55 (4): 427–450. S2CID 32293255. arXiv:1711.01477  . doi:10.1090/bull/1616. 
  19. ^ Vladimir Voevodsky (2014) Experimental library of univalent formalization of mathematics
  20. ^ Kapulkin, Chris; Lumsdaine, Peter LeFanu. The Simplicial Model of Univalent Foundations. arXiv:1211.2851   [math.LO]. 
  21. ^ Shulman, Michael. Univalence for inverse diagrams and homotopy canonicity. Mathematical Structures in Computer Science. 2015, 25 (5): 1203–1277. S2CID 13595170. arXiv:1203.3253  . doi:10.1017/S0960129514000565. 
  22. ^ Martín Hötzel Escardó (October 18, 2018) A self-contained, brief and complete formulation of Voevodsky’s Univalence Axiom
  23. ^ Bezem, M.; Coquand, T.; Huber, S. A model of type theory in cubical sets (PDF). 
  24. ^ Altenkirch, Thorsten; Kaposi, Ambrus, A syntax for cubical type theory (PDF) 
  25. ^ V. Voevodsky, Univalent Foundations Project (a modified version of an NSF grant application), p. 9

參考來源

編輯
  1. ^ Thierry Coquand (2014) Univalent Foundation and Constructive Mathematics[15] [16]
  2. ^ But see Martín Hötzel Escardó's approach.[22]:4-6

外部連結

編輯
形式化數學庫

Template:Foundations-footer

取自 "https://zh.wikipedia.org/w/index.php?title=泛等基础&oldid=81593282"