Skip navigation
Please use this identifier to cite or link to this item:
Title: Univalence, Foundations and Philosophy: With a Sheaf-Shaped Appendix
Authors: Tsementzis, Dimitris
Advisors: Halvorson, Hans
Burgess, John
Contributors: Philosophy Department
Keywords: Foundations of Mathematics
Homotopy Type Theory
Set Theory
Type Theory
Univalent Foundations
Subjects: Philosophy
Issue Date: 2016
Publisher: Princeton, NJ : Princeton University
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...
Alternate format: The Mudd Manuscript Library retains one bound copy of each dissertation. Search for these copies in the library's main catalog:
Type of Material: Academic dissertations (Ph.D.)
Language: en
Appears in Collections:Philosophy

Files in This Item:
File Description SizeFormat 
Tsementzis_princeton_0181D_11901.pdf1.77 MBAdobe PDFView/Download

Items in Dataspace are protected by copyright, with all rights reserved, unless otherwise indicated.