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.

Bruno Bentzen is an assistant professor of philosophy at Zhejiang University. His work revolves around the philosophy of logic and mathematics, with a particular emphasis on the tradition of mathematical intuitionism and constructive type theory. He has published a number of articles in some of the most prestigious journals in logic and philosophy of mathematics (Review of Symbolic Logic, Notre Dame Journal of Formal Logic, Philosophia Mathematica, History and Philosophy of Logic, Erkenntnis). In addition to a few logic conference papers, his interdisciplinary research can also be found in leading journals in other areas, ranging from phenomenology to computer science (Husserl Studies, Mathematical Structures in Computer Science). He is the first author of the edited book "Logics for AI and Law" published by College Publications in 2023.

Before joining Zhejiang University in 2021, he held postdoctoral positions at Carnegie Mellon University working with Jeremy Avigad and the Czech Academy of Sciences working with Ansten Klev. Currently, he is also a core member of the Zhejiang University–University of Luxembourg Joint Lab on Advanced Intelligent Systems and Reasoning together with Beishui Liao and Leon van der Torre.