Constructing Fully Complete Models of Multiplicative Linear Logic

TL;DR

This paper shows how to construct fully complete categorical models of the multiplicative fragment of Linear Logic using the Hyland-Tan double glueing technique, applicable to many degenerate models.

Contribution

It introduces a tensor calculus for compact closed categories with biproducts and demonstrates how glueing yields fully complete models, unifying various existing models.

Findings

Hyland-Tan double glueing produces fully complete models

Tensor calculus for compact closed categories developed

Unification of multiple models from literature

Abstract

The multiplicative fragment of Linear Logic is the formal system in this family with the best understood proof theory, and the categorical models which best capture this theory are the fully complete ones. We demonstrate how the Hyland-Tan double glueing construction produces such categories, either with or without units, when applied to any of a large family of degenerate models. This process explains as special cases a number of such models from the literature. In order to achieve this result, we develop a tensor calculus for compact closed categories with finite biproducts. We show how the combinatorial properties required for a fully complete model are obtained by this glueing construction adding to the structure already available from the original category.