A Note on Bisimulation Quantifiers and Fixed Points over Transitive Frames

We consider some basic questions regarding the expressive power of two extensions of the modal language: the one with bisimulation quantifiers and the one with extremal fixed points. If we interpret formulas over all models, the two extensions differ: the first one does not increase the expressive power of the modal language, while the second is expressively equivalent to the μ-calculus. But this weakness of bisimulation quantifiers is lost when we restrict to models based on classes of transitive frames. Here, bisimulation quantifiers are stronger than fixed points, and it makes sense to ask whether the two extensions are expressively equivalent. This equivalence is already known for certain classes of transitive frames, and we shall investigate how it is related with the property of uniform interpolation of the corresponding modal logic. We prove that in general the two extensions are not equivalent, although they are so for the classes of transitive and transitive and reflexive frames.