An Infinitary Treatment of Full Mu-Calculus

We explore the proof theory of the modal mu-calculus with converse, aka the 'full mu-calculus'. Building on nested sequent calculi for tense logics and infinitary proof theory of fixed point logics, a cut-free sound and complete proof system for full mu-calculus is proposed. As a corollary of our framework, we also obtain a direct proof of the regular model property for the logic: every satisfiable formula has a tree model with finitely many distinct subtrees. To obtain the results we appeal to the basic theory of well-quasi-orderings in the spirit of Kozen's proof of the finite model property for mu-calculus without converse.