The mu-calculus' Alternation Hierarchy is Strict over Non-Trivial Fusion Logics

TL;DR

This paper proves that the strictness of the mu-calculus' alternation hierarchy extends to non-trivial fusion logics, highlighting the hierarchy's complexity in multimodal contexts.

Contribution

It demonstrates the strictness of the mu-calculus' alternation hierarchy over non-trivial fusion of modal logics, extending known results beyond Kripke frames.

Findings

Hierarchy is strict over non-trivial fusion logics

Collapse of mu-calculus occurs in specific multimodal logics

Hierarchy remains strict in multimodal settings

Abstract

The modal mu-calculus is obtained by adding least and greatest fixed-point operators to modal logic. Its alternation hierarchy classifies the mu-formulas by their alternation depth: a measure of the codependence of their least and greatest fixed-point operators. The mu-calculus' alternation hierarchy is strict over the class of all Kripke frames: for all n, there is a mu-formula with alternation depth n+1 which is not equivalent to any formula with alternation depth n. This does not always happen if we restrict the semantics. For example, every mu-formula is equivalent to a formula without fixed-point operators over S5 frames. We show that the multimodal mu-calculus' alternation hierarchy is strict over non-trivial fusions of modal logics. We also comment on two examples of multimodal logics where the mu-calculus collapses to modal logic.