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.