2026-09-15T15:40:13Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:25441 2026-09-05T19:16:34Z ddc:004 open_access

A Uniform Cut-Elimination Theorem for Linear Logics with Fixed Points and Super Exponentials Saurin, Alexis Bauer, Esaïe cut elimination exponential modalities fixed-points linear logic light logics mu-calculus non-wellfounded proofs proof theory sequent calculus subexponentials super exponentials In the realm of light logics deriving from linear logic, a number of variants of exponential rules have been investigated. The profusion of such proof systems induces the need for cut-elimination theorems for each logic, the proofs of which may be redundant. A number of approaches in proof theory have been adopted to cope with this need. In the present paper, we consider this issue from the point of view of enhancing linear logic with least and greatest fixed-points and considering such a variety of exponential connectives. Our main contribution is to provide a uniform cut-elimination theorem for a parametrized system with fixed-points by combining two approaches: cut-elimination proofs by reduction (or translation) to another system and the identification of sufficient conditions for cut-elimination. More precisely, we examine a broad range of systems, taking inspiration from Nigam and Miller’s subexponentials and from the first author and Laurent’s super exponentials. Our work is motivated, on the one hand, by Baillot’s work on light logics with recursive types and on the other hand by our recent work on the proof theory of the modal μ-calculus. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Alexis Saurin and Esaïe Bauer 2026 Is Part Of LIPIcs, Volume 363, 34th EACSL Annual Conference on Computer Science Logic (CSL 2026) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.CSL.2026.17 urn:nbn:de:0030-drops-254418 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2026.17 eng https://creativecommons.org/licenses/by/4.0/legalcode