On the cut-elimination of the modal μ-calculus: Linear Logic to the rescue

2025/06/11 by Esaïe Bauer, Alexis Saurin, Bauer, Esaïe +1 · 1 citation
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems

paper · pdf · doi:10.48550/arxiv.2506.09791

openalex publication_date 2025/06/11 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/30

Abstract

This paper presents a proof-theoretic analysis of the modal μ-calculus. 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, \muLLmodinf, 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 \muLLmodinf 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.

Citations

• A Linear-logical Reconstruction of Intuitionistic Modal Logic S4
• Least and Greatest Fixed Points in Linear Logic

Cited by

• Cut-elimination for the alternation-free modal mu-calculus

Related

• Cut-elimination for the alternation-free modal mu-calculus
• Cut elimination for a non-wellfounded system for the master modality
• A journey in modal proof theory: From minimal normal modal logic to discrete linear temporal logic
• Demystifying μ
• The mu-calculus' Alternation Hierarchy is Strict over Non-Trivial Fusion Logics