An Infinitary Treatment of Full Mu-Calculus

Abstract

We explore the proof theory of the modal µ -calculus with converse, aka the ‘fullµ -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 µ -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 µ -calculus without converse.