Does HoTT Provide a Foundation for Mathematics? by James Ladyman (University of Bristol, UK)

Talk at: FOMUS 2016. For all Talks and more information, slides etc. see: http://fomus.weebly.com/

Does HoTT Provide a Foundation for Mathematics? by James Ladyman (University of Bristol, UK)

Abstract: Homotopy Type Theory (HoTT) is a putative new foundation for mathematics grounded in constructive intensional type theory, that offers an alternative to the foundations provided by ZFC set theory and category theory. This paper explains and motivates an account of how to define, justify and think about HoTT in a way that is self-contained, and argues that so construed it is a candidate for being an autonomous foundation for mathematics. We first consider various questions that a foundation for mathematics might be expected to answer, and find that the standard formulation of HoTT as presented in the `HoTT Book' does not answer many of them. More importantly, the presentation of HoTT given in the HoTT Book is not 'autonomous' since it explicitly depends upon other fields of mathematics. In particular, an important rule for the treatment of identity in HoTT is path induction, which is commonly explained by appeal to the homotopy interpretation of the theory’s types, tokens, and identities as (respectively) spaces, points, and paths. However, if HoTT is to be an autonomous foundation then such an interpretation cannot play a fundamental role. We offer a derivation of path induction, motivated from pre-mathematical considerations, without recourse to homotopy theory. We use this as part of an alternative presentation of HoTT that does not depend upon ideas from other parts of mathematics, and in particular makes no reference to homotopy theory (but is compatible with the homotopy interpretation), and argue that it is a candidate autonomous foundation for mathematics. Our elaboration of HoTT is based on an interpretation of types as mathematical concepts, which accords with the intensional nature of the type theory.
This workshop was organised with the generous support of the Association for Symbolic Logic (ASL), the Association of German Mathematicians (DMV), the Berlin Mathematical School (BMS), the Center of Interdisciplinary Research (ZiF), the Deutsche Vereinigung für Mathematische Logik und für Grundlagenforschung der Exakten Wissenschaften (DVMLG), the German Academic Merit Foundation (Stipendiaten machen Programm), the Fachbereich Grundlagen der Informatik of the German Informatics Society (GI) and the German Society for Analytic Philosophy (GAP).

Видео Does HoTT Provide a Foundation for Mathematics? by James Ladyman (University of Bristol, UK) канала FOMUS 2016