泛等基础

维基百科，自由的百科全书

泛等基础是一种建立数学基础的方法，它以类型作为构建数学结构的基础对象。泛等基础中的类型并不完全对应于集合论基础中的任何东西，但它们都可以视作一个空间，其中相等类型对应于同伦等价空间，类型的相等元素对应于由路径（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”