Tuesday, 13 February 2001
2:30 - 4:00 R.A.G. Seely
A Logic of a Linear Functor
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 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. In general, "bunched logics" correspond to block (functor) logics with little restriction on nesting. We finish by showing how to translate between the two styles of logic.