  The polyadic mu-calculus is a modal fixpoint logic whose formulas define
relations of nodes rather than just sets in labelled transition systems. It can
express exactly the polynomial-time computable and bisimulation-invariant
queries on finite graphs. In this paper we show a hierarchy result with respect
to expressive power inside the polyadic mu-calculus: for every level of
fixpoint alternation, greater arity of relations gives rise to higher
expressive power. The proof uses a diagonalisation argument.
