Quantitative Equality in Substructural Logic via Lipschitz Doctrines
Francesco Dagnino, Fabio Pasquali
TL;DR
The paper tackles the problem of giving a meaningful, quantitative notion of equality in substructural logic by reframing equality as a Lipschitz-like distance within Lawvere's doctrine framework. It develops an $R$-graded, Lipschitz extension of a minimal Linear Logic fragment augmented with graded modalities $!_r$, providing a deductive calculus and sound, complete categorical semantics, together with a 2-categorical analysis that yields a universal 2-comonad construction for generating models. Key contributions include formalizing $R$-Lipschitz doctrines and a calculus for quantitative equality, establishing their coalgebraic semantics, and clarifying the relation to standard equality via left adjoints while connecting to Quantitative Equational Theories (QETs). The approach is illustrated through metric-space and quantitative realizability instantiations and is shown to extend smoothly to richer substructural logics up to full Linear Logic with quantifiers, offering a principled bridge between quantitative reasoning and substructural logics.
Abstract
Substructural logics naturally support a quantitative interpretation of formulas, as they are seen as consumable resources. Distances are the quantitative counterpart of equivalence relations: they measure how much two objects are similar, rather than just saying whether they are equivalent or not. Hence, they provide the natural choice for modelling equality in a substructural setting. In this paper, we develop this idea, using the categorical language of Lawvere's doctrines. We work in a minimal fragment of Linear Logic enriched by graded modalities, which are needed to write a resource sensitive substitution rule for equality, enabling its quantitative interpretation as a distance. We introduce both a deductive calculus and the notion of Lipschitz doctrine to give it a sound and complete categorical semantics. The study of 2-categorical properties of Lipschitz doctrines provides us with a universal construction, which generates examples based for instance on metric spaces and quantitative realisability. Finally, we show how to smoothly extend our results to richer substructural logics, up to full Linear Logic with quantifiers.