## First Order Linear Logic in Symmetric Monoidal Closed
Categories

**Simon Ambler**
*Abstract:* There has recently been considerable interest
in the development of `logical frameworks' which can represent many
of the logics arising in computer science in a uniform way. Within
the Edinburgh LF project, this concept is split into two
components; the first being a general proof theoretic encoding of
logics, and the second a uniform treatment of their model theory.
This thesis forms a case study for the work on model theory.

The models of many first and higher order logics can be
represented as *fibred* or *indexed* categories with
certain extra structure, and this has been suggested as a general
paradigm. The aim of the thesis is to test the strength and
flexibility of this paradigm by studying the specific case of
Girard's linear logic . It should be noted that the exact form of
this logic in the first order case is not entirely certain, and the
system treated here is significantly different to that considered
by Girard.

To secure a good class of models, we develop a carefully
restricted form of first order intuitionistic linear logic, called
*L_{FOLL}*, in which the linearity of the logic is also
reflected at the level of types. That is, the terms of the logic
are given by a *linear tyoe theory* LTT corresponding to the
algebraic idea of a symmetric monoidal closed category. The study
of logic in such categories is motivated by two examples which are
derived as linear analogues of presheaf topoi and Heyting valued
sets respectively. We introduce the concept of a *monoidal
factorisation system* over such categories to provide a basis
for a theory of linear predicates. A monoidal factorisation system
then gives rise to a structure preserving fibration between
symmetric monoidal closed categories, which we term a *linear
doctrine*. We provide a sequent calculus formulation of
*L_{FOLL}* and show that it is both sound and complete with
respect to a linear doctrine semantics.

Although the logic *L_{FOLL}* sits nicely within the fibred
category framework, we note that it also displays some quite
unexpected features which should be of interest in future work on
both the categorical semantics of linear logic and model theory in
the general case.

**PhD Thesis - Price £8.00**

*LFCS report ECS-LFCS-92-194 (also published as
CST-87-92)*

Previous |

Index |

Next