Applications of methods of proof theory in category theory. (Q2744122)

The book is a considerably extended version of the author's ph.d. thesis published as a monograph. It develops the approach to the study of closed categories of various types (cartesian closed, symmetric monoidal closed, biclosed etc.) based on use of natural deduction and lambda-terms in the spirit of \textit{G. Mints}' works.NEWLINENEWLINENEWLINEIt consists of an introduction and 5 chapters: 1) Basic notions; 2) Equality of canonical morphisms and a coherence theorem in CC-categories; 3) Deciding algorithm for equality of canonical morphisms in SMC-categories; 4) Equality of canonical morphisms in biclosed categories; 5) A necessary and sufficient condition of equivalence of deductions of a balanced sequent in \(N^{SMC}\) and \(N^{BC}\). Canonical morphisms here may be regarded as morphisms in a free closed category of corresponding type. NEWLINENEWLINENEWLINEChapter 2 contains the following coherence theorem: if \(a,b:A\to B\) are canonical maps in CC-categories and the sequent \(A\to B\) is balanced then \(a=b\). This result was first published by \textit{A. A. Babaev} and \textit{S. V. Solov'ev} [Zap. Nauchn. Semin. Leningr. Otd. Mat. Inst. Steklova 88, 3-29 (1979; Zbl 0429.03037)]. A simplified proof of this theorem may be found in the monograph by \textit{A. S. Troelstra} and \textit{H. Schwichtenberg} [``Basic proof theory'', Cambridge Tracts Theor. Comput. Sci. 43 (2000; Zbl 0957.03053)].NEWLINENEWLINENEWLINEChapter 3 studies in detail a certain system of \(\lambda\)-terms for SMC-categories (and also, in modern terminology, a multiplicative fragment of intuitionistic linear logic) first sketched by \textit{G. E. Mints} [Zap. Nauchn. Semin. Leningr. Otd. Mat. Inst. Steklova 68, 83-114 (1977; Zbl 0368.02036)]. It is shown that two canonical morphisms are equal iff the corresponding terms are equivalent. A deciding algorithm for equivalence based on a certain normalization strategy is suggested. An interesting aspect of the system in question is that, in difference of the approach using the let construction in treatment of \(\otimes\), it uses the projection symbols as in ordinary terms with pairing, but the use of these symbols is subject to certain restrictions (a kind of `coupling').NEWLINENEWLINENEWLINEChapter 4 deals with biclosed categories in the way similar to SMC-categories (using a translation of the system for biclosed categories to the system for SMC-categories). Its results were earlier presented in the paper of \textit{A. A. Babaev} [Zap. Nauchn. Semin. Leningr. Otd. Mat. Inst. Steklova 105, 3-9 (1981; Zbl 0474.18002)].NEWLINENEWLINENEWLINEChapter 5 suggests a necessary and sufficient condition of equality of canonical morphisms in SMC- and BC-categories based on the syntactical structure of corresponding \(\lambda\)-terms. The condition does not require normalization. It is inspired by the work of \textit{R. Voreadou} [``Coherence and non-commutative diagrams in closed categories'', Mem. Am. Math. Soc. 182 (1977; Zbl 0347.18008)].NEWLINENEWLINENEWLINETaking into account that the book is published in Russian, two other publications in English that were used as sources may be mentioned: \textit{A. A. Babaev} [Proc. Steklov Inst. Math. 193, 29-35 (1993); translation from Tr. Mat. Inst. Steklova 193, 31-36 (1992; Zbl 0801.18007)] and \textit{A. A. Babaev} [``Equality of canonical morphisms in biclosed categories'', Izv. Akad Nauk Azerb. 5, 17-20 (1999)].NEWLINENEWLINENEWLINEBibliography contains very little references after 1990, for example, the author probably has no access to the works on intuitionistic linear logic and related term systems (one may mention such authors as \textit{G. Bierman}, \textit{N. Ghani}, \textit{V. de Paiva}).