Cut Elimination in Categories

Proof theory and category theory were first drawn together by Lambek some 30 years ago but, until now, the most fundamental notions of category theory (as opposed to their embodiments in logic) have not been explained systematically in terms of proof theory. Here it is shown that these notions, in p...

Full description

Bibliographic Details
Main Author: Dosen, K.
Format: eBook
Language:English
Published: Dordrecht Springer Netherlands 1999, 1999
Edition:1st ed. 1999
Series:Trends in Logic, Studia Logica Library
Subjects:
Online Access:
Collection: Springer Book Archives -2004 - Collection details see MPG.ReNa
LEADER 02387nmm a2200337 u 4500
001 EB000722068
003 EBX01000000000000000575150
005 00000000000000.0
007 cr|||||||||||||||||||||
008 140122 ||| eng
020 |a 9789401712071 
100 1 |a Dosen, K. 
245 0 0 |a Cut Elimination in Categories  |h Elektronische Ressource  |c by K. Dosen 
250 |a 1st ed. 1999 
260 |a Dordrecht  |b Springer Netherlands  |c 1999, 1999 
300 |a XII, 229 p  |b online resource 
505 0 |a 2. Functors -- 3. Natural Transformations -- 4. Adjunctions -- 5. Comonads -- 6. Cartesian Categories -- Conclusion -- References 
653 |a Symbolic and Algebraic Manipulation 
653 |a Computer science / Mathematics 
653 |a Mathematical logic 
653 |a Logic 
653 |a Algebra, Homological 
653 |a Category Theory, Homological Algebra 
653 |a Mathematical Logic and Foundations 
041 0 7 |a eng  |2 ISO 639-2 
989 |b SBA  |a Springer Book Archives -2004 
490 0 |a Trends in Logic, Studia Logica Library 
028 5 0 |a 10.1007/978-94-017-1207-1 
856 4 0 |u https://doi.org/10.1007/978-94-017-1207-1?nosfx=y  |x Verlag  |3 Volltext 
082 0 |a 160 
520 |a Proof theory and category theory were first drawn together by Lambek some 30 years ago but, until now, the most fundamental notions of category theory (as opposed to their embodiments in logic) have not been explained systematically in terms of proof theory. Here it is shown that these notions, in particular the notion of adjunction, can be formulated in such as way as to be characterised by composition elimination. Among the benefits of these composition-free formulations are syntactical and simple model-theoretical, geometrical decision procedures for the commuting of diagrams of arrows. Composition elimination, in the form of Gentzen's cut elimination, takes in categories, and techniques inspired by Gentzen are shown to work even better in a purely categorical context than in logic. An acquaintance with the basic ideas of general proof theory is relied on only for the sake of motivation, however, and the treatment of matters related to categories is also in general self contained. Besides familiar topics, presented in a novel, simple way, the monograph also contains new results. It can be used as an introductory text in categorical proof theory