Syntactic cut-elimination for a fragment of the modal mu-calculus

Abstract: For some modal fixed point logics, there are deductive systems that enjoy syntactic cut-elimination. An early example is the system in Pliuskevicius (1991) for LTL. More recent examples are the systems by the authors of this paper for the logic of common knowledge (Brünnler and Studer, 2009) and by Hill and Poggiolesi (2010) for PDL, which are based on a form of deep inference. These logics can be seen as fragments of the modal mu-calculus. Here we are interested in how far this approach can be pushed in general. To this end, we introduce a nested sequent system with syntactic cut-elimination which is incomplete for the modal mu-calculus, but complete with respect to a restricted language that allows only fixed points of a certain form. This restricted language includes the logic of common knowledge and PDL. There is also a traditional sequent system for the modal mu-calculus by Jäger et al. (2008) , without a syntactic cut-elimination procedure. We embed that system into ours and vice versa, thus establishing cut-elimination also for the shallow system, when only the restricted language is considered. [Copyright &y& Elsevier]