On the proof theory of the modal mu-calculus (Q1005937)

The paper investigates two cut-free infinitary deduction systems for the modal \(\mu\)-calculus. The first one is the system \(T^\omega_{\mu+}\), introduced by \textit{G. Jäger, M. Kretz} and \textit{T. Studer} [J. Log. Algebr. Program. 76, No.~2, 270--292 (2008; Zbl 1156.68013)], which includes a variant of an infinitary \(\omega\)-rule. The second one is \(T^{\text{pre}}_\mu\), which is an adaptation to modal \(\mu\)-calculus of a proof system by \textit{C. Dax, M. Hofmann} and \textit{M. Lange} [Lect. Notes Comput. Sci. 4337, 273--284 (2006; Zbl 1163.03308)] for the linear-time \(\mu\)-calculus; it has finitary rules, but allows infinite branches in proof trees under certain conditions. The main result of the paper is a translation of \(T^\omega_{\mu+}\)-proofs to \(T^{\text{pre}}_\mu\)-proofs. As a corollary, it also gives a new proof of completeness of \(T^{\text{pre}}_\mu\) and of the finite model property of the modal \(\mu\)-calculus.