The categorical study of linear logic is addressed in this chapter. Specifically, the author demonstrates that a particular functor pertaining to the abstract categorical model of linear logic can be constructed in purely proof-theoretical terms.
Linear logic was introduced as a means to study the dynamics of proofs in classical logic, although some ideas from intuitionistic logic were taken into account in its conception. Regarding category theory, it is well known that monoidal closed categories provide models of intuitionistic linear logic, whereas *-autonomous categories provide a model for classical linear logic.
Chu’s construction was introduced in the appendix of Barr [1], with purely categorical interests, as a method to build a *-autonomous category starting from monoidal closed categories, several years before Girard’s seminal paper [2] was published. The goal of this chapter is to show that the action of a particular functor existing in Chu’s construction can be represented by Girard’s trips on a proof-net of linear logic.
This chapter is part of an edited book, but it seems that it was not subject to a thorough proofreading process; a considerable number of typographical and other minor errors appear throughout the text, including the references.