Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

LNL polycategories and doctrines of linear logic

Michael Shulman

TL;DR

This work introduces LNL polycategories as a unifying semantic framework for linear logic with exponentials, combining nonlinear cartesian and linear symmetric polycategorical structures linked by storage modalities. It formalizes LNL doctrines to capture families of universal properties and shows that many classical structures (e.g., LNL adjunctions, linearly distributive categories with storage, CBPV, Freyd-categories) arise as algebras for such doctrines. The authors develop a doctrinal approach via sketches and small-object completions to construct free algebras, and they derive a sequent calculus that presents these free categories. They also prove that doctrine mappings yield pseudo 2-adjunctions between categories of models and introduce sorted and Kleisli-type theories to model a variety of polarized and storage-rich calculi. The framework provides a modular, syntactic–semantic bridge connecting substructural logics with their categorical models, enabling uniform comparisons and constructions across diverse logical systems.

Abstract

We define and study LNL polycategories, which abstract the judgmental structure of classical linear logic with exponentials. Many existing structures can be represented as LNL polycategories, including LNL adjunctions, linear exponential comonads, LNL multicategories, IL-indexed categories, linearly distributive categories with storage, commutative and strong monads, CBPV-structures, models of polarized calculi, Freyd-categories, and skew multicategories, as well as ordinary cartesian, symmetric, and planar multicategories and monoidal categories, symmetric polycategories, and linearly distributive and *-autonomous categories. To study such classes of structures uniformly, we define a notion of LNL doctrine, such that each of these classes of structures can be identified with the algebras for some such doctrine. We show that free algebras for LNL doctrines can be presented by a sequent calculus, and that every morphism of doctrines induces an adjunction between their 2-categories of algebras.

LNL polycategories and doctrines of linear logic

TL;DR

This work introduces LNL polycategories as a unifying semantic framework for linear logic with exponentials, combining nonlinear cartesian and linear symmetric polycategorical structures linked by storage modalities. It formalizes LNL doctrines to capture families of universal properties and shows that many classical structures (e.g., LNL adjunctions, linearly distributive categories with storage, CBPV, Freyd-categories) arise as algebras for such doctrines. The authors develop a doctrinal approach via sketches and small-object completions to construct free algebras, and they derive a sequent calculus that presents these free categories. They also prove that doctrine mappings yield pseudo 2-adjunctions between categories of models and introduce sorted and Kleisli-type theories to model a variety of polarized and storage-rich calculi. The framework provides a modular, syntactic–semantic bridge connecting substructural logics with their categorical models, enabling uniform comparisons and constructions across diverse logical systems.

Abstract

We define and study LNL polycategories, which abstract the judgmental structure of classical linear logic with exponentials. Many existing structures can be represented as LNL polycategories, including LNL adjunctions, linear exponential comonads, LNL multicategories, IL-indexed categories, linearly distributive categories with storage, commutative and strong monads, CBPV-structures, models of polarized calculi, Freyd-categories, and skew multicategories, as well as ordinary cartesian, symmetric, and planar multicategories and monoidal categories, symmetric polycategories, and linearly distributive and *-autonomous categories. To study such classes of structures uniformly, we define a notion of LNL doctrine, such that each of these classes of structures can be identified with the algebras for some such doctrine. We show that free algebras for LNL doctrines can be presented by a sequent calculus, and that every morphism of doctrines induces an adjunction between their 2-categories of algebras.

Paper Structure

This paper contains 9 sections, 41 theorems, 56 equations, 2 figures, 3 tables.

Table of Contents

  1. Introduction
  2. lnl polycategories
  3. Relation to the literature
  4. Unifying universality
  5. Doctrines and sketches
  6. Sorted doctrines
  7. The doctrinal completion of a sketch
  8. The sequent calculus of a doctrine
  9. Adjunctions induced by doctrine maps

Key Result

Proposition 2.9

[][][][][][][][][][]thm:univ-uniq If $\psi \in \cP(\Theta\mid \Gamma\mathbin{;} \Delta,A)$ and $\psi' \in \cP(\Theta\mid \Gamma\mathbin{;} \Delta,A')$ are universal in $A$ and $A'$ respectively, then there is a unique isomorphism $\phi : A\cong A'$ such that $\phi \circ_A \psi = \psi'$; and similarl

Figures (2)

  • Figure 1: Diagram for \ref{['thm:extremal-fibcomp']}
  • Figure 2: LNL Sequent calculus

Theorems & Definitions (135)

  • Definition 2.1
  • Definition 2.2
  • Remark 2.3
  • Remark 2.4
  • Remark 2.5
  • Remark 2.6
  • Remark 2.7
  • Definition 2.8
  • Proposition 2.9
  • proof
  • ...and 125 more