Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy

Description

"The old logic put thought in fetters, while the new logic gives it wings." For the past century, philosophers working in the tradition of Bertrand Russell - who promised to revolutionise philosophy by introducing the 'new logic' of Frege and Peano - have employed predicate logic as their formal language of choice. In this book, Dr David Corfield presents a comparable revolution with a newly emerging logic - modal homotopy type theory. Homotopy type theory has recently been developed as a new foundational language for mathematics, with a strong philosophical pedigree. Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy offers an introduction to this new language and its modal extension, illustrated through innovative applications of the calculus to language, metaphysics, and mathematics. The chapters build up to the full language in stages, right up to the application of modal homotopy type theory to current geometry. From a discussion of the distinction between objects and events, the intrinsic treatment of structure, the conception of modality as a form of general variation to the representation of constructions in modern geometry, we see how varied the applications of this powerful new language can be. Cover Modal Homotopy Type Theory: The Prospect of a New Logic for Philosophy Copyright Preface Contents Chapter 1: A Path to a New Logic 1.1 First Encounters 1.2 Next Steps 1.3 Encounters with Ordinary Language Philosophy Definitional Equality Propositional Equality 1.4 Quadrature 1.5 Conclusion Chapter 2: Dependent Types 2.1 The Need for Types 2.2 The Analogy between Logic and Arithmetic 2.3 Dependent Sum and ‘and’ 2.4 Dependent Types 2.5 Context and Dependency Structure 2.6 Events as Basic Types 2.7 Revisiting the Philosophical Literature Chapter 3: Homotopy Types 3.1 Introduction 3.2 HoTT Components 3.2.1 Identity Types 3.2.2 The Type Hierarchy 3.2.3 The Univalence Axiom 3.2.4 Higher Inductive Types 3.3 Definite Description in Natural Language 3.3.1 Definite Description for any Type 3.3.2 Definite Description for Dependent Types 3.4 The Structure of A 3.4.1 Places in a Structure 3.4.2 Types Equipped with Structure 3.4.3 The Complex Numbers 3.5 Conclusion Chapter 4: Modal Types 4.1 Modalities as Monads 4.2 Towards Modal HoTT 4.2.1 General Types 4.2.2 First-order Modal Logic and Barcan 4.2.3 Contexts and Counterfactuals 4.3 Temporal Type Theory 4.4 Mode Theory Chapter 5: Spatial Types 5.1 Introduction 5.2 Current Geometry 5.3 Regaining the Philosophy of Geometry 5.3.1 Weyl: The Essence of Space 5.3.2 Cassirer: Beyond Intuition 5.4 Capturing Modern Geometry 5.5 Geometry in Modal HoTT 5.6 Simplicity and Representability in Modal HoTT 5.7 Conclusion Chapter 6: Conclusion Further Reading Category Theory Type Theory Homotopy Type Theory Modal Type Theory Miscellaneous References Index