+612 9045 4394
Introduction to Higher-Order Categorical Logic : Cambridge Studies in Advanced Mathematics, 7 - J. Lambek

Introduction to Higher-Order Categorical Logic

Cambridge Studies in Advanced Mathematics, 7


Published: 26th September 1988
RRP $81.95
This title is not in stock at the Booktopia Warehouse and needs to be ordered from our supplier.
Click here to read more about delivery expectations.

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.

'A readable and timely account of important results, most of which were not previously available in book form.' Bulletin of the London Mathematical Society

Introduction to category theory
Introduction to Part 0p. 3
Categories and functorsp. 4
Natural transformationsp. 8
Adjoint functorsp. 12
Equivalence of categoriesp. 16
Limits in categoriesp. 19
Triplesp. 27
Examples of cartesian closed categoriesp. 35
Cartesian closed categories and [lambda]-calculus
Introduction to Part Ip. 41
Historical perspective on Part Ip. 42
Propositional calculus as a deductive systemp. 47
The deduction theoremp. 50
Cartesian closed categories equationally presentedp. 52
Free cartesian closed categories generated by graphsp. 55
Polynomial categoriesp. 57
Functional completeness of cartesian closed categoriesp. 59
Polynomials and Kleisli categoriesp. 62
Cartesian closed categories with coproductsp. 65
Natural numbers objects in cartesian closed categoriesp. 68
Typed [lambda]-calculip. 72
The cartesian closed category generated by a typed [lambda]-calculusp. 77
The decision problem for equalityp. 81
The Church-Rosser theorem for bounded termsp. 84
All terms are boundedp. 88
C-monoidsp. 93
C-monoids and cartesian closed categoriesp. 98
C-monoids and untyped [lambda]-calculusp. 101
A constructionp. 107
Historical comments on Part Ip. 114
Type theory and toposes
Introduction to Part IIp. 123
Historical perspective on Part IIp. 124
Intuitionistic type theoryp. 128
Type theory based on equalityp. 133
The internal language of a toposp. 139
Peano's rules in a toposp. 145
The internal language at workp. 148
The internal language at work IIp. 153
Choice and the Boolean axiomp. 160
Topos semanticsp. 164
Topos semantics in functor categoriesp. 169
Sheaf categories and their semanticsp. 177
Three categories associated with a type theoryp. 186
The topos generated by a type theoryp. 189
The topos generated by the internal languagep. 193
The internal language of the topos generatedp. 196
Toposes with canonical subobjectsp. 200
Applications of the adjoint functors between toposes and type theoriesp. 205
Completeness of higher order logic with choice rulep. 212
Sheaf representation of toposesp. 217
Completeness without assuming the rule of choicep. 223
Some basic intuitionistic principlesp. 226
Further intuitionistic principlesp. 231
The Freyd cover of a toposp. 237
Historical comments on Part IIp. 244
Supplement to Section 17p. 250
Representing numerical functions in various categories
Introduction to Part IIIp. 253
Recursive functionsp. 253
Representing numerical functions in cartesian closed categoriesp. 257
Representing numerical functions in toposesp. 264
Representing numerical functions in C-monoidsp. 271
Historical comments on Part IIIp. 277
Bibliographyp. 279
Author indexp. 289
Subject indexp. 291
Table of Contents provided by Syndetics. All Rights Reserved.

ISBN: 9780521356534
ISBN-10: 0521356539
Series: Cambridge Studies in Advanced Mathematics, 7
Audience: Professional
Format: Paperback
Language: English
Number Of Pages: 304
Published: 26th September 1988
Country of Publication: GB
Dimensions (cm): 22.86 x 15.88  x 1.91
Weight (kg): 0.45