Logical questions concerning the μ-calculus: Interpolation, Lyndon and Łoś-Tarski

Abstract

The (modal) μ-calculus ([14]) is a very powerful extension of modal logic with least and greatest fixed point operators. It is of great interest to computer science for expressing properties of processes such as termination (every run is finite) and fairness (on every infinite run, no action is repeated infinitely often to the exclusion of all others).The power of the μ-calculus is also evident from a more theoretical perspective. The μ-calculus is a fragment of monadic second-order logic (MSO) containing only formulae that are invariant for bisimulation, in the sense that they cannot distinguish between bisimilar states. Janin and Walukiewicz prove the converse: any property which is invariant for bisimulation and MSO-expressible is already expressible in the μ-calculus ([13]). Yet the μ-calculus enjoys many desirable properties which MSO lacks, like a complete sequent-calculus ([29]), an exponential-time decision procedure, and the finite model property ([25]). Switching from MSO to its bisimulation-invariant fragment gives us these desirable properties.In this paper we take a classical logician's view of the μ-calculus. As far as we are concerned a new logic should not be allowed into the community of logics without at least considering the standard questions that any logic is bothered with. In this paper we perform this rite of passage for the μ-calculus. The questions we will be concerned with are the following.