On the cut-elimination of the modal $μ$-calculus: Linear Logic to the rescue
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866912424978808832 |
|---|---|
| author | Bauer, Esaïe Saurin, Alexis |
| author_facet | Bauer, Esaïe Saurin, Alexis |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2506_09791 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | On the cut-elimination of the modal $μ$-calculus: Linear Logic to the rescue Bauer, Esaïe Saurin, Alexis Logic in Computer Science 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. |
| title | On the cut-elimination of the modal $μ$-calculus: Linear Logic to the rescue |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2506.09791 |