A Modern Perspective on Type Theory: From its Origins until Today (Applied Logic Series Book 29)

This book provides an overview of type theory. The first part of the book is historical, yet at the same time, places historical systems in the modern setting. The second part deals with modern type theory as it developed since the 1940s, and with the role of propositions as types (or proofs as terms. The third part proposes new systems that bring more advantages together. Contents......Page 6 Part I......Page 12 Part II......Page 14 Part III......Page 15 Acknowledgements......Page 16 Avoiding the paradox in set theory......Page 18 Avoiding the paradox in type theory......Page 21 The approach......Page 22 I: The Evolution of Type Theory until the 1940s......Page 24 1 Prehistory......Page 26 1a: Paradox threats......Page 27 1b: Paradox threats in formal systems......Page 28 2 Type theory in Principia Mathematica......Page 36 2a: Principia’s propositional functions......Page 39 2b: The Ramified Theory of Types RTT......Page 52 2c: Properties of RTT......Page 66 2d: Legal propositional functions......Page 76 Conclusions......Page 82 3 Deramification......Page 86 3a: History of the deramification......Page 87 3b: The Simple Theory of Types STT......Page 93 3c: Are orders to be blamed?......Page 98 Conclusions......Page 117 II: Propositions as Types, Pure Type Systems, AUTOMATH......Page 120 4 Propositions as Types and Pure Type Systems......Page 122 4a: Propositions as Types and Proofs as Terms (PAT)......Page 123 4b: Lambda calculus......Page 129 4c: Pure Type Systems......Page 133 5a: RTT in PAT style......Page 142 5b: STT in PAT style......Page 167 Conclusions......Page 168 6 A Correspondence between RTT and the system Nuprl......Page 170 6a: On the role of orders......Page 171 6b: The Nuprl type system......Page 173 6c: RTT in Nuprl......Page 185 Conclusions......Page 190 7 Automath......Page 196 7a: Description of AUTOMATH......Page 199 7b; From AUT-68 towards a PTS......Page 211 7c: λ68......Page 217 7d: More Suitable Pure Type Systems for AUTOMATH......Page 240 Conclusions......Page 246 III: Extensions of Pure Type Systems......Page 248 8 Pure Type Systems with definitions......Page 250 8a: Definitions in contexts......Page 251 8b: Definitions in the terms and the contexts......Page 255 Conclusions......Page 257 9 The Barendregt cube with parameters......Page 260 9a: On parameters in the Barendregt cube......Page 261 9b: The Barendregt cube refined with parameters......Page 267 Conclusions......Page 270 10 Pure Type Systems with parameters and definitions......Page 272 10a: Parametric constants and definitions......Page 273 10b: Properties of terms......Page 287 10c: Properties of legal terms......Page 298 10d: Restrictive use of parameters......Page 307 10e: Systems in the refined Barendregt cube......Page 315 10f: First-order predicate logic......Page 320 Conclusions: Yet another extension of PTSs?......Page 324 Aa: Pure Type Systems......Page 328 Ab: The Barendregt cube......Page 329 Ac: The Ramified Theory of Types......Page 331 Ad: The Simple Theory of Types......Page 335 Ae: Church’s simply typed λ-calculus λ[sub(→Church)]......Page 338 Af: A fragment of Nuprl in PTS-style......Page 339 Ag: AUTOMATH......Page 341 Ah: Pure Type Systems with definitions......Page 345 Ai: Pure Type Systems with parametric constants......Page 349 Aj: A CD-PTS and its subsystems......Page 350 Bibliography......Page 354 C......Page 366 F......Page 367 L......Page 368 P......Page 369 S......Page 370 W......Page 371 R......Page 372 Z......Page 373 List of Figures......Page 374 `Towards the end of the nineteenth century, Frege gave us the abstraction principles and the general notion of functions. Self-application of functions was at the heart of Russell's paradox. This led Russell to introduce type theory in order to avoid the paradox. Since, the twentieth century has seen an amazing number of theories concerned with types and functions and many applications. Progress in computer science also meant more and more emphasis on the use of logic, types and functions to study the syntax, semantics, design and implementation of programming languages and theorem provers, and the correctness of proofs and programs. The authors of this book have themselves been leading the way by providing various extensions of type theory which have been shown to bring many advantages. This book gathers much of their influential work and is highly recommended for anyone interested in type theory. The main emphasis is on: - Types: from Russell to Ramsey, to Church, to the modern Pure Type Systems and some of their extensions. - Functions: from Frege, to Russell to Church, to Automath and the use of functions in mathematics, programming languages and theorem provers. - The role of types in logic: Kripke's notion of truth, the evolution and role of the propositions as types concept and its use in logical frameworks. - The role of types in computation: extensions of type theories which can better model proof checkers and programming languages are given. The first part of the book is historical, yet at the same time, places historical systems (like Russell's RTT) in the modern setting. The second part deals with modern type theory as it developed since the 1940s, and with the role of propositions as types (or proofs as terms), but at the same time, places another historical system (the proof checker Automath) in the modern setting. The third part uses this bridging in the first two parts between historical and modern systems to propose new systems that bring more advantages together. This book has much to offer to mathematicians, logicians and to computer scientists in general. It will have considerable influence for many years to come.' - Henk Barendregt "This first part of the book is historical, yet at the same time, places historical systems (like Russell's RTT) in the modern setting. The second part deals with modern type theory as it developed since the 1940s, and with the role of propositions as types (or proofs as terms), but at the same time, places another historical system (the proof checker Automath) in the modern setting. The third part uses this bridging in the first two parts between historical modern setting. The third part uses this bridging in the first two parts between historical and modern systems to propose new systems that bring more advantages together. This book has much to offer to mathematicians, logicians and to computer scientists in general."--Jacket The explicit and formal use of types (and thus an early form of what is presently called "type theory") was originally intended to prevent the paradoxes that occurred in logic and mathematics at the end of the 19th and the beginning of the 20th century.