Categorical Linear Logic and Linear Distributivity

Abstract

Linear logic was introduced by Girard in 1987 as a sub-structural logic that retains the constructivism of intuitionistic logic and the symmetry of classical logic. The categorical semantics of linear logic subsequently became an active area of research. In 1992, Cockett and Seely introduced linearly distributive categories (LDC) as semantics for the multiplicative fragment of linear logic. These categories take multiplicative conjunction (tensor) and disjunction (par), along with their interaction via linear distributivities, as the primitive categorical concepts. This highlighted the importance of linear distributivity which provide precisely necessary structure to model the logical cut rule. The theory of LDCs has continued to develop and remains an active area of research within categorical linear logic.

This thesis explores two key areas of categorical linear logic and linear distributivity that have received less attention in recent years, but remain important and worthy of further investigation. The first concerns the relationship between linear distributivity and cartesian structures. This was central topic in the early development of LDCs, notably with the introduction of cartesian linearly distributive categories (CLDC), but their study was quickly abandoned. Moreover, Cockett, Koslowski and Seely introduced linear bicategories in 2000, the bicategorical analogue of LDCs, as natural categorical semantics for non-commutative linear logic. Despite their promising theoretical foundation, further development in this direction was limited. However, recent efforts in categorical logic, particular in classical logic and relational semantics, have renewed interest and highlighted the need for continued research in these directions.

The study of linear distributivity and cartesian structures presented includes the development of a linearly distributive analogue to the Fox theorem, a central result in monoidal category theory characterizing cartesian categories, and a re-examination of CLDCs, which investigates their unique properties and the possible classes of examples. The study of linear bicategories was reinvigorated through the construction of previously unrecognized examples,by leveraging the theory of quantales and quantaloids within the framework of categorical linear logic.