Effective cut-elimination for a fragment of modal mu-calculus (Q454366): Difference between revisions

The mu-calculus is an extension of temporal logic for transition systems with added fixpoint operators which appeared particularly useful for specification and verification of temporal properties. An infinitary system adequate for the whole mu-calculus was proved cut-free in a non-constructive way by \textit{G. Jäger}, \textit{M. Kretz} and \textit{T. Studer} in [J. Log. Algebr. Program. 76, No. 2, 270--292 (2008; Zbl 1156.68013)]. A constructive proof of cut elimination for the fragment of mu-calculus, called \(\mathrm{M}_1\), with non-iterated fixpoints and omega-rule was offered by \textit{W. Buchholz} in [Arch. Math. Logic 40, No. 4, 255--272 (2001; Zbl 1007.03051)], but only for positive formulas. In this paper, G. Mints provides another constructive proof of cut elimination for \(\mathrm{M}_1\) which improves Buchholz's result in two ways. First, it is not restricted to proofs of positive formulas. Second, the omega-rule is only an intermediate tool for obtaining a cut-free calculus. In order to remove cut from \(\mathrm{M}_1\), the system \(\mathrm{M}^\prime\) is introduced, which is cut-free but uses instead of the (finitary) rule (ind) of \(\mathrm{M}_1\) some infinitary rule. Next, the auxiliary system \(\mathrm{M}^\Omega \) is introduced which adds to \(\mathrm{M}^\prime\) two omega-rules and a form of cut. It is shown that every derivation in \(\mathrm{M}_1\) is transformed into a derivation in \(\mathrm{M}^\Omega \), and every derivation in \(\mathrm{M}^\Omega \) is transformed into a derivation in \(\mathrm{M}^\prime\). Although this result by itself does not imply cut admissibility for \(\mathrm{M}_1\), there are simple sufficient conditions satisfied by Mints's proof which recovers provability in the finitary system from provability in the infinitary one. As a result, cut admissibility for \(\mathrm{M}_1\) follows. The text is rather dense and technical, hence the reader not acquainted with the mu-calculus should first consult some introductory paper, e.g., \textit{J. Bradfield} and \textit{C. Stirling}'s survey in [``Modal mu-calculus'', in: Handbook of modal logic. Amsterdam: Elsevier. 721--756 (2007; Zbl 1114.03001)].