The logic of linear functors

by Richard Blute, J.R.B. Cockett, and R.A.G. Seely

This paper describes a family of logics whose categorical semantics is based on functors with structure rather than on categories with structure. This allows the consideration of logics which contain possibly distinct logical subsystems whose interactions are mediated by functorial mappings. For example, within one unified framework, we shall be able to handle logics as diverse as modal logic, ordinary linear logic, and the "noncommutative logic" of Abrusci and Ruet, a variant of linear logic which has both commutative and noncommutative connectives.
Although this paper will not consider in depth the categorical basis of this approach to logic, preferring instead to emphasize the syntactic novelties that it generates in the logic, we shall focus on the particular case when the logics are based on a linear functor, to give a definite presentation of these ideas. However, it will be clear that this approach to logic has considerable generality.
There have been several individual attempts to develop logics with distinct but related subsystems of connectives, such as the Abrusci--Ruet noncommutative logic and the bunch logic of O'Hearn and Pym; generally these are presented in terms of "bunching" the formulas in the sequents of the logics via different "punctuation". The present functor logic, by contrast, uses a system of "formula blocks", which represent the functorial action and which give finer control over what logical features may be displayed. By displaying a family of functor logics, we illustrate how different logical systems can be developed along these lines, logics which are primarily distinguished by the degree to which they permit nesting of formula blocks. Our examples will include a basic logic where there is essentially no nesting, a system of linear modal logic, which allows nesting, but has only one system of connectives, and the Abrusci--Ruet logic, where nesting is virtually unrestricted and there are two subsystems of connectives. We finish by showing how to translate between the ``bunch'' style of logic and our ``formula block'' or functor logic using the Abrusci--Ruet noncommutative logic as an example.