Cut elimination in categories
type: Item
instance of: scholarly article
title: Cut elimination in categories
zbMATH Open document ID: 0981.03068
author: Kosta Došen
published in: Trends in Logic -- Studia Logica Library
publication date: 2000-01-04T00:00:00Z
review text: The book is an introduction to categorical proof theory. After the presentation of basic notions (category, functor, natural transformation) from the proof-theoretical point of view, main attention is paid to the notion of adjunction together with the related notion of comonad (one may as well consider monads). It is shown that all these notions can be formulated in such a way that the (standard) equalities between arrows are necessary and sufficient conditions for the composition (i.e., cut) elimination in freely generated structures corresponding to these notions. This means, in particular, that every arrow in categories involved in freely generated adjunctions and comonads can be represented by a term that does not contain composition. Moreover, such a term has normal form unique for the arrow. The composition-free normal form serves also to demonstrate that strengthening the notions of adjunction and comonad with any new equality between arrows would trivialize these notions. The difference between these composition-free formulations of categorical notions and standard formulation is that natural transformations are not conceived as families of arrows, but as operations on arrows. The book has an introduction and six chapters. In chapter 1 cut elimination in free categories generated by arbitrary graphs is considered. (In the form of ``cut disintegration'', which is local in contrast to Gentzen's global approach.) In chapter 2 it is shown how the notion of functor (and semifunctor) can be characterized by ``cut disintegration''. In chapter 3 the same approach is developed for natural transformations. Chapter 4 is central for the book. In this chapter free adjunctions are considered. In chapter 5 the author considers free comonads (from a logical point of view they precede in a way the monads). These chapters contain a survey and comparison of existing definitions of adjunction and comonad. Their behaviour w.r.t. cut elimination is studied. As an application of c…
Mathematics Subject Classification ID: 03G30
Mathematics Subject Classification ID: 18A15
Mathematics Subject Classification ID: 03F05
Mathematics Subject Classification ID: 18A40
Mathematics Subject Classification ID: 03-02
Mathematics Subject Classification ID: 18-02
zbMATH DE Number: 1382802
zbMATH Keywords: cut elimination
zbMATH Keywords: categories with structure
zbMATH Keywords: adjointness
zbMATH Keywords: comonad
zbMATH Keywords: categorical proof theory
reviewed by: Serguei V. Solov'ev
MaRDI profile type: Publication
description: scientific article; zbMATH DE number 1382802