登录 EN

添加临时用户

同伦类型论作为结构主义数学基础的研究

Homotopy Type Theory as a Structuralist Foundation of Mathematics

作者:孙振宇
  • 学号
    2013******
  • 学位
    硕士
  • 电子邮箱
    ale******com
  • 答辩日期
    2016.05.31
  • 导师
    王巍
  • 学科名
    哲学
  • 页码
    87
  • 保密级别
    公开
  • 培养单位
    070 社科学院
  • 中文关键词
    同伦类型论,范畴论,数学基础,结构主义,不变量
  • 英文关键词
    homotopy type theory,category theory,foundations of mathematics,mathematical structuralism,invariant

摘要

数学结构主义是一种哲学立场,即认为数学是研究抽象结构的学科。这一哲学立场业已激发了对数学本体论和知识论的深刻研究,本文试图从一个不同的角度——数学实践的角度——去探讨结构主义的方法论特征。作为数学实践中的方法论原则,结构主义的立场体现为“同构的对象同一”。本文试图探讨这一方法论原则在集合论数学基础、范畴论数学基础中的具体体现。特别地,本文指出该原则对于基于集合论的数学基础是外在的、不相容的,而范畴论数学基础则可以提供一个内在的、从顶到底的结构主义方法论环境。 同伦类型论建立在对内涵Martin-L?f类型论的同伦拓扑解释之上,其目标是建立“以计算为基础的数学”。带有单价公理的同伦类型论可以提供区别于传统集合论和范畴论数学基础的一个全新数学基础(称作“单价基础”)的备选者。本文探讨了结构主义方法论原则在同伦类型论中的具体体现,并指出与范畴论基础的情况类似,同伦类型论同样提供了一个内在的结构主义方法论环境。这一特征是由单价公理所保证的,由不变量原则所体现的。 本文还提出以不变量作为整合数学结构主义的中枢概念,并论证了它同时涵盖了范畴论结构主义、在物结构主义的核心特征,并且进一步启发了对其逆过程——去不变量或范畴化——进行哲学探究的可能性。

Mathematical structuralism is a philosophical position that mathematics is all about the study of abstract structures rather than concrete objects. This position motivates profound studies into ontology and epistemology of mathematical entities. But our research focuses on a different aspect of mathematical structuralism, namely, its methodological features related with mathematical practices. As a methodological principle, the slogan of structuralism is “isomorphic objects are identical”. Our research tries to investigate the practical embodiment of this principle in different well-developed foundations of mathematics, such as set-theoretical and categorical ones. We argue that this principle is exogenous of and incompatible with set theoretical foundations, while categorical foundations could provide an endogenous and top-down methodological environment for mathematical structuralism. Homotopy type theory is based on the homotopical interpretations of intentional Martin-L?f type theories and aims to establish a foundation of mathematics bases on computation. Homotopy type theory with Voevodsky’s univalent axiom (a.k.a. univalent foundation) could possibly provide a new foundation of mathematics while is different with traditional foundations such as ZFC and ETCS. Our research also investigates the practical embodiment of structuralist principle in univalent foundation, and argues that just as the case of category theory, homotopy type theory provides an intrinsic methodological environment for mathematical structuralism. And this feature is guaranteed by the univalent axiom while represented by the invariant principle. Our research further advocates that we should take the notion of invariant to be the central concept of mathematical structuralism, since this notion integrates the essential characteristics of categorical and in rebus structuralism. And we could do some future research on the philosophical impacts of its inverse process known as “de-invariant” or categorification.