Please use this identifier to cite or link to this item: http://arks.princeton.edu/ark:/88435/dsp015h73pz547
 Title: Univalence, Foundations and Philosophy: With a Sheaf-Shaped Appendix Authors: Tsementzis, Dimitris Advisors: Halvorson, HansBurgess, John Contributors: Philosophy Department Keywords: Foundations of MathematicsHomotopy Type TheorySet TheoryStructuralismType TheoryUnivalent Foundations Subjects: PhilosophyLogic 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... URI: http://arks.princeton.edu/ark:/88435/dsp015h73pz547 Alternate format: The Mudd Manuscript Library retains one bound copy of each dissertation. Search for these copies in the library's main catalog: catalog.princeton.edu Type of Material: Academic dissertations (Ph.D.) Language: en Appears in Collections: Philosophy

Files in This Item:
File Description SizeFormat