On the cut-elimination of the modal $\mu$-calculus: Linear Logic to the rescue

TL;DR

This paper introduces a new linear logic-based system for the modal $d$-calculus, enabling syntactic cut-elimination through a novel translation and proof-theoretic analysis.

Contribution

It presents dLLmodinf{}, a linear logic system that facilitates cut-elimination for the modal d-calculus by integrating modalities with linear logic's exponential modalities.

Findings

Proved cut-elimination for dLLmodinf{}

Developed a linear translation of modal d-calculus proofs

Established a proof-theoretic framework for non-wellfounded modal d-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, \muLLmodinf{}, 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 \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.