Univalence, Foundations and Philosophy: With a Sheaf-Shaped Appendix

Abstract

The Univalent Foundations (UF) of mathematics provide a foundation for mathematics entirely independent from Cantorian set theory. This development raises important questions: In what sense is UF a new foundation? How does it relate to set theory? How can it be justified philosophically? It also raises fundamental methodological questions about analytic philosophy: how are we to justify the pervasive use of first-order logic and set theory when confronted with a foundation of mathematics in which neither plays an essential role? This dissertation aims to answer all these questions.

In Chapter 1, I orient my project by investigating the relation between philosophy, the foundations of mathematics and formal logic. Then, in Chapter 2 I argue that UF is better-able to live up to the ideal of a structuralist foundation than other proposals and respond to several challenges against the foundational aspirations of UF.

In the next two chapters I compare UF to other foundational proposals. In Chapter 3 I argue for a pluralistic picture between UF and ZFC, examine the extent to which Homotopy Type Theory can receive a pre-formal “meaning explanation” independent of set theory and respond to a potent objection raised by Hellman and Shapiro against non-set-theoretic foundations of mathematics. In Chapter 4 I examine alternative structuralist foundations and argue that Makkai’s Type-Theoretic Categorical Foundations of Mathematics (TTCFM) emerges as the most serious contender to UF. I then compare UF and TTCFM on several fronts, including on their intended semantics (∞-groupoids vs. ∞-categories), offering an argument in favour of ∞-groupoids as the basic objects of a structuralist foundation.

In the final chapter I develop a mathematical logic (“n-logic”) for UF by extending Makkai’s system of First-Order Logic with Dependent Sorts (FOLDS). I define the syntax and proof system for n-logic, prove soundness with respect to both homotopy-theoretic and set-theoretic semantics, and sketch some applications. This establishes a mathematical logic for UF that provides the groundwork for a new kind of formal philosophy. And after that comes the time, in the evening light, to dance...