Should Type Theory Replace Set Theory as the Foundation of Mathematics?

Axiomathes 33 (1):1-13 (2023)
  Copy   BIBTEX

Abstract

Mathematicians often consider Zermelo-Fraenkel Set Theory with Choice (ZFC) as the only foundation of Mathematics, and frequently don’t actually want to think much about foundations. We argue here that modern Type Theory, i.e. Homotopy Type Theory (HoTT), is a preferable and should be considered as an alternative.

Categories

Keywords

Reprint years

DOI

10.1007/s10516-023-09676-0

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 92,197

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

Naïve Type Theory.Thorsten Altenkirch - 2019 - In Stefania Centrone, Deborah Kant & Deniz Sarikaya (eds.), Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts. Springer Verlag. pp. 101-136.
Set-Theoretic Foundations.Stewart Shapiro - 2000 - The Proceedings of the Twentieth World Congress of Philosophy 6:183-196.
The Importance of Developing a Foundation for Naive Category Theory.Marcoen J. T. F. Cabbolet - 2015 - Thought: A Journal of Philosophy 4 (4):237-242.
A Simple Type Theory With Partial Functions And Subtypes.William M. Farmer - 1993 - Annals of Pure and Applied Logic 64 (3):211-240.
Reflections on the Foundations of Mathematics: Univalent Foundations, Set Theory and General Thoughts.Stefania Centrone, Deborah Kant & Deniz Sarikaya (eds.) - 2019 - Springer Verlag.
On the Proof-theoretic Foundation of General Definition Theory.Lars Hallnäs - 2006 - Synthese 148 (3):589-602.
A Transfinite Type Theory with Type Variables. [REVIEW]J. M. P. - 1966 - Review of Metaphysics 20 (1):144-144.
A simple type theory with partial functions and subtypes11Supported by the MITRE-Sponsored Research program. Presented at the 9th International Congress of Logic, Methodology and Philosophy of Science held in Uppsala, Sweden, August 7-14, 1991. [REVIEW]William M. Farmer - 1993 - Annals of Pure and Applied Logic 64 (3):211-240.
Does Homotopy Type Theory Provide a Foundation for Mathematics?James Ladyman & Stuart Presnell - 2016 - British Journal for the Philosophy of Science:axw006.
Expressing ‘the structure of’ in homotopy type theory.David Corfield - 2017 - Synthese 197 (2):681-700.
Math, Science,?M. Kary - 2009 - Axiomathes 19 (3):321-339.
Homotopy Type Theory and Structuralism.Teruji Thomas - 2014 - Dissertation, University of Oxford
Editorial Preface: Thought Experiments in Mathematics.Evandro Agazzi & Marco Buzzoni - 2023 - Global Philosophy 33 (1):1-5.
Identity in HoTT, Part I.James Ladyman & Stuart Presnell - 2015 - Philosophia Mathematica 23 (3):386-406.
The Type Theory of Law: An Essay in Psychoanalytic Jurisprudence.Marko Novak - 2016 - Cham: Imprint: Springer.

Analytics

Added to PP
2023-02-14

Downloads
29 (#553,499)

6 months
15 (#170,787)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

No citations found.

Add more citations

References found in this work

No references found.

Add more references