000			01663nam a22002537a 4500
999			_c54779 _d54779
008			210322b ||||| |||| 00| 0 eng d
020			_a9780521356534
082			_a512.55 _bLAM
100			_aLambek, Joachim
245			_aIntroduction to higher-order categorical logic
260			_aCambridge: _bCambridge University Press, _c1986.
300			_aix, 293 p. : ill. ; _bpb. ; _c24 cm.
365			_aGBP _b48.99
440			_aCambridge studies in advanced mathematics ; 7
504			_aIncludes indexes. Bibliography: p. [279]-288.
520			_aIn 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.
650			_aCategories (Mathematics)
650			_aCartesian Closed Categories and Calculus
650			_aNumerical Functions in Various Categories
650			_aAlgebra
650			_aMathematics
700			_aScott, P. J
942			_cTD