The µ-calculus’ collapse on variations of S5

Abstract

The mu-calculus is obtained by adding to modal logic the least and greatest fixed-point operators mu and nu. The alternation depth of a formula measures the entanglement of its least and greatest fixed-point operators. Bradfield showed that, for all natural number n, there is a formula such that has alternation depth n and, over all Kripke frames, is not equivalent to any formula with alternation depth smaller than n.

The same may not happen over restricted classes of frames: Alberucci and Facchini showed that, over frames of S5, every mu-formula is equivalent to a formula without fixed point operators. In this case, we say the mu-calculus collapses to modal logic over frames of S5.

We show how Alberucci and Facchini’s proof generalize to the mu-calculus’s collapse over frames of intuitionistic S5. This generalization can also be done for some non-normal logics and for graded modal logics. We also show that, on the other hand, the S5-calculus does not collapse over the bimodal logic S5_2.