Introduction to Higher-Order Categorical Logic

Front Cover
Cambridge University Press, Mar 25, 1988 - Mathematics - 293 pages
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.
 

Contents

I
3
II
4
III
8
IV
12
V
16
VI
19
VII
27
VIII
35
XXXIII
133
XXXIV
139
XXXV
145
XXXVI
148
XXXVII
153
XXXVIII
160
XXXIX
164
XL
169

IX
41
X
42
XI
47
XII
50
XIII
52
XIV
55
XV
57
XVI
59
XVII
62
XVIII
65
XIX
68
XX
72
XXI
77
XXII
81
XXIII
84
XXIV
88
XXV
93
XXVI
98
XXVII
101
XXVIII
107
XXIX
114
XXX
123
XXXI
124
XXXII
128
XLI
177
XLII
186
XLIII
189
XLIV
193
XLV
196
XLVI
200
XLVII
205
XLVIII
212
XLIX
217
L
223
LI
226
LII
231
LIII
237
LIV
244
LV
250
LVI
253
LVIII
257
LX
264
LXI
271
LXII
277
LXIII
279
LXIV
289
LXV
291
Copyright

Other editions - View all

Common terms and phrases

Bibliographic information