On the cut-elimination of the modal $$\mu $$-calculus: Linear Logic to the rescue
Esaïe Bauer, Alexis Saurin · Lecture notes in computer science · 2025
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.