Philosophical Type Theory - Bruno Bentzen

This book offers solutions to traditional philosophical problems against the background of type theory as its deductive system. If philosophical logic is the branch of philosophy that focuses on the application of logical methods to address philosophical problems, then, in this narrow sense, "philosophical type theory" centers on essentially type-theoretic answers to such problems. Guided by a computational view of type theory developed mainly after Brouwer, Bishop, and Constable, this book launches the program of philosophical type theory by focusing on an analysis of a selection of central problems, including the sense-reference and analytic-synthetic distinctions as well as the status of identity in univalent foundations. Emphasis is also given to comparisons and contrasts with past views by Kant, Bolzano, Frege, Dummett, Martin-Löf, Voevodsky, and others throughout the book, making it of great interest to scholars and graduate students who have a keen interest in the areas of philosophy, logic, mathematics, and computer science.