On the cut-elimination of the modal µ-calculus: Linear Logic to the rescue
Esaïe Bauer, Alexis Saurin · HAL (Le Centre pour la Communication Scientifique Directe) · 2024
This paper presents a proof-theoretic analysis of the modal µ-calculus, well-known in verification theory and relevant to the model-checking problem. More precisely, we prove a syntactic cut-elimination for the non-wellfounded modal µ-calculus, using methods from linear logic and its exponential modalities. To achieve this, we introduce a new system, µLL∞□ , which is a linear version of the modal µ-calculus, intertwining the modalities from the modal µ-calculus with the exponential modalities from linear logic. Our strategy for proving cut-elimination involves (i)proving cut-elimination for µLL∞□ and (ii) translating proofs of the modal µ-calculus into this new system via a "linear translation," allowing us to extract the cut-elimination result.