Introduction to Higher-Order Categorical Logic

✍ Scribed by J. Lambek, P.J. Scott

• Publisher: Cambridge University Press
• Year: 1986
• Tongue: English
• Leaves: 303
• Series: Cambridge Studies in Advanced Mathematics 7
• Category: Library

✦ Synopsis

In this volume, Lambek and Scott reconcile two different viewpoints of the foundations of mathematics, namely mathematical logic and category theory. In Part I, they show that typed lambda-calculi, a formulation of higher-order logic, and cartesian closed categories, are essentially the same. Part II demonstrates that another formulation of higher-order logic, (intuitionistic) type theories, is closely related to topos theory. Part III is devoted to recursive functions. Numerous applications of the close relationship between traditional logic and the algebraic language of category theory are given. The authors have included an introduction to category theory and develop the necessary logic as required, making the book essentially self-contained. Detailed historical references are provided throughout, and each section concludeds with a set of exercises.

✦ Table of Contents

Cover......Page 1
Title page......Page 3
Contents......Page 5
Preface......Page 7
0 Introduction to category theory......Page 11
Introduction to Part 0......Page 13
1 Categories and functors......Page 14
2 Natural transformations......Page 18
3 Adjoint functors......Page 22
4 Equivalence of categories......Page 26
5 Limits in categories......Page 29
6 Triples......Page 37
7 Examples of cartesian closed categories......Page 45
I Cartesian closed categories and λ-calculus......Page 49
Introduction to Part I......Page 51
Historical perspective on Part I......Page 52
1 Propositional calculus as a deductive system......Page 57
2 The deduction theorem......Page 60
3 Cartesian closed categories equationally presented......Page 62
4 Free cartesian closed categories generated by graphs......Page 65
5 Polynomial categories......Page 67
6 Functional completeness of cartesian closed categories......Page 69
7 Polynomials and Kleisli categories......Page 72
8 Cartesian closed categories with coproducts......Page 75
9 Natural numbers objects in cartesian closed categories......Page 78
10 Typed λ-calculi......Page 82
11 The cartesian closed category generated by a typed λ-calculus......Page 87
12 The decision problem for equality......Page 91
13 The Church-Rosser theorem for bounded terms......Page 94
14 All terms are bounded......Page 98
15 C-monoids......Page 103
16 C-monoids and cartesian closed categories......Page 108
17 C-monoids and untyped λ-calculus......Page 111
18 A construction by Dana Scott......Page 117
Historical comments on Part I......Page 124
II Type theory and toposes......Page 131
Introduction to Part II......Page 133
Historical perspective on Part II......Page 134
1 Intuitionistic type theory......Page 138
2 Type theory based on equality......Page 143
3 The internal language of a topos......Page 149
4 Peano's rules in a topos......Page 155
5 The internal language at work......Page 158
6 The internal language at work II......Page 163
7 Choice and the Boolean axiom......Page 170
8 Topos semantics......Page 174
9 Topos semantics in functor categories......Page 179
10 Sheaf categories and their semantics......Page 187
11 Three categories associated with a type theory......Page 196
12 The topos generated by a type theory......Page 199
13 The topos generated by the internal language......Page 203
14 The internal language of the topos generated......Page 206
15 Toposes with canonical subobjects......Page 210
16 Applications of the adjoint functors between toposes and type theories......Page 215
17 Completeness of higher order logic with choice rule......Page 222
18 Sheaf representation of toposes......Page 227
19 Completeness without assuming the rule of choice......Page 233
20 Some basic intuitionistic principles......Page 236
21 Further intuitionistic principles......Page 241
22 The Freyd cover of a topos......Page 247
Historical comments on Part II......Page 254
Supplement to Part II, Section 17......Page 260
III Representing numerical functions in various categories......Page 261
1 Recursive functions......Page 263
2 Representing numerical functions in cartesian closed categories......Page 267
3 Representing numerical functions in toposes......Page 274
4 Representing numerical functions in C-monoids......Page 281
Historical Comments on Part III......Page 287
Bibliography......Page 289
Author index......Page 299
Subject index......Page 301