Framework captures complex multi-output logical reasoning with graph structures
A Fibrational Framework For Multi-Conclusion Logics
Logic in Computer Science
Summary
Logical systems often use trees to represent reasoning with single conclusions. This work by the authors expands this to handle multiple conclusions by using graphs instead of trees, allowing for more complex reasoning patterns. They develop rules and prove important properties like how to combine and simplify reasoning steps. Their framework links to known logical systems and offers new ways to understand logical reasoning structures through advanced category theory concepts.
What this means in practice
- •For programming language designers: Use the framework to model advanced type systems that handle both linear and non-linear resources with multiple conclusions.
- •For proof assistant implementers: Incorporate the multi-output sequent calculus to extend proof systems managing both linear and classical logic components.
A theory result. No direct application yet.
Authors
Oualid Merzouga
Abstract
The fibrational framework of Licata, Shulman, and Riley gives a uniform account of substructural and modal logics for single-conclusion judgments. This thesis extends it to a multiple-output setting in which cartesian resources may be used freely, while linear resources occur exactly once on either side of the turnstile. Judgments are indexed by descriptors: directed acyclic graphs generalizing the tree-shaped expressions of the original framework. Descriptor $2$-cells encode structural transformations, and explicit gates provide weakening, contraction, coweakening, and cocontraction at linear modes. We define a sequent calculus generated by two connectives, $F$ and $U$. We prove identity, invertibility, and cut admissibility. The mode and type theories present linear-non-linear $2$-polycategories, and the projection is a local discrete fibration and a fibration, with opcartesian lifts for one-output base morphisms. Two adequacy results validate the framework: its cartesian fragment recovers the Licata--Shulman--Riley calculus, and its purely linear fragment presents classical multiplicative linear logic. Finally, we relate indexed and fibrational semantics. After developing representability correspondences for multicategories and polycategories, we establish an equivalence between multi-indexed categories over a fixed representable base and multicategorical opfibrations over it, together with its biclosed bifibrational version. We also give a one-way construction from planar poly-indexed data to a planar polycategory.