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, Hans Burgess, John |

Contributors: | Philosophy Department |

Keywords: | Foundations of Mathematics Homotopy Type Theory Set Theory Structuralism Type Theory Univalent Foundations |

Subjects: | Philosophy Logic |

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 | Size | Format | |
---|---|---|---|---|

Tsementzis_princeton_0181D_11901.pdf | 1.77 MB | Adobe PDF | View/Download |

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