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.

Abstract This paper presents a proof-theoretic analysis of the modal $$\mu $$ μ -calculus. More precisely, we prove a syntactic cut-elimination for the non-wellfounded modal $$\mu $$ μ -calculus, using methods from linear logic. and its exponential modalities. To achieve this, we introduce a new system, $$\mu \textsf {LL}_{\Box }^{\infty }$$ μ LL □ ∞ , which is a linear version of the modal $$\mu $$ μ -calculus, intertwining the modalities from the modal $$\mu $$ μ -calculus with the exponential modalities from linear logic. Our strategy for proving cut-elimination involves (i) proving cut-elimination for $$\mu \textsf {LL}_{\Box }^{\infty }$$ μ LL □ ∞ and (ii) translating proofs of the modal mu-calculus into this new system via a “linear translation”, allowing us to extract the cut-elimination result.