A Linear/Producer/Consumer Model of Classical Linear Logic

TL;DR

This paper introduces a new proof- and category-theoretic framework for classical linear logic that distinguishes linear, producer, and consumer regimes, providing a unified semantic model and proving key metatheoretic properties.

Contribution

It presents the LPC framework, a novel logic that separates reasoning into three regimes and connects them via category-theoretic structures, extending Benton's linear/non-linear logic.

Findings

LPC corresponds to a system of three categories with adjunctions.

Admissibility theorems for cut and duality rules are established.

Concrete instances of the LPC model are provided.

Abstract

This paper defines a new proof- and category-theoretic framework for classical linear logic that separates reasoning into one linear regime and two persistent regimes corresponding to ! and ?. The resulting linear/producer/consumer (LPC) logic puts the three classes of propositions on the same semantic footing, following Benton's linear/non-linear formulation of intuitionistic linear logic. Semantically, LPC corresponds to a system of three categories connected by adjunctions reflecting the linear/producer/consumer structure. The paper's metatheoretic results include admissibility theorems for the cut and duality rules, and a translation of the LPC logic into category theory. The work also presents several concrete instances of the LPC model.