2026-07-23T06:19:40Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:22789 2025-10-02T11:32:03Z ddc:004 open_access

A Mixed Linear and Graded Logic: Proofs, Terms, and Models Vollmer, Victoria Marshall, Danielle Eades III, Harley Orchard, Dominic linear logic graded modal logic adjoint decomposition Graded modal logics generalise standard modal logics via families of modalities indexed by an algebraic structure whose operations mediate between the different modalities. The graded "of-course" modality !_r captures how many times a proposition is used and has an analogous interpretation to the of-course modality from linear logic; the of-course modality from linear logic can be modelled by a linear exponential comonad and graded of-course can be modelled by a graded linear exponential comonad. Benton showed in his seminal paper on Linear/Non-Linear logic that the of-course modality can be split into two modalities connecting intuitionistic logic with linear logic, forming a symmetric monoidal adjunction. Later, Fujii et al. demonstrated that every graded comonad can be decomposed into an adjunction and a "strict action". We give a similar result to Benton, leveraging Fujii et al.’s decomposition, showing that graded modalities can be split into two modalities connecting a graded logic with a graded linear logic. We propose a sequent calculus, its proof theory and categorical model, and a natural deduction system which we show is isomorphic to the sequent calculus system. Interestingly, our system can also be understood as Linear/Non-Linear logic composed with an action that adds the grading, further illuminating the shared principles between linear logic and a class of graded modal logics. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Victoria Vollmer and Danielle Marshall and Harley Eades III and Dominic Orchard 2025 Is Part Of LIPIcs, Volume 326, 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2025.32 urn:nbn:de:0030-drops-227892 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2025.32 eng https://creativecommons.org/licenses/by/4.0/legalcode