A categorical interpretation of logical derivations and some of its applications in algebra

Antoine El Khoury (1) , Sergei Soloviev (1, 2) , Laurent Mehats (3) , Mark Spivakovsky (4)

1 IRIT-ACADIE - Assistance à la Certification d’Applications DIstribuées et Embarquées
2 ITMO - National Research University of Information Technologies, Mechanics and Optics [St. Petersburg]
3 LaBRI - Laboratoire Bordelais de Recherche en Informatique
4 IMT - Institut de Mathématiques de Toulouse UMR5219

We consider certain applications of proof theory to the study of algebraic categories, The case usually studied in the literature is that of free categories with an additional structure. In this paper, we consider several problems in nonfree categories, such as the problem of full coherence, the problem of dependency of diagrams, the problem of description of arbitrary natural transformations, which show that the applications of proof theory to categories may go much farther.

Domaines: Logique en informatique [cs.LO]

Antoine El Khoury, Sergei Soloviev, Laurent Mehats, Mark Spivakovsky. A categorical interpretation of logical derivations and some of its applications in algebra. Journal of Mathematical Sciences, 2010, 168 (3), pp.491-503. ⟨10.1007/s10958-010-0002-2⟩. ⟨hal-00727359⟩