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.
Author(s): Fairouz Kamareddine, Twan Laan, Rob Nederpelt
Series: Applied Logic Series 29
Year: 2004
Language: English
Pages: 377
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
