On the Proof Theory of the Constructive Modal μ-Calculus

We study the constructive modal μ-calculus μCK, an intuitionistic version of modal logic extended with least and greatest fixed points. In addition to providing the Kripke-style and game semantics from the literature for this logic, we develop an ill-founded sequent calculus for μCK, where derivation can be potentially infinite in height, but are additionally constrained by a global trace condition to ensure soundness. Recent work by Curzi and Leigh propose a general cut elimination procedure for ill-founded proof systems based on Tait’s and Girard’s reducibility candidates. This method is displayed on an one-sided sequent calculus for a fragment of linear logic. We modify this method for the context of μCK. Our main result is a cut elimination theorem for μCK, providing a showcase of this method adapted for a logic with modalities, a two-sided sequent calculus and limited interdefinability between its connectives. With this, we contribute to a general cut elimination procedure for ill-founded proof systems.