On the expressive power of monadic least fixed point logic

Monadic least fixed point logic MLFP is a natural logic whose expressiveness lies between that of first-order logic FO and monadic second-order logic MSO. In this paper, we take a closer look at the expressive power of MLFP. Our results are: (1) MLFP can describe graph properties beyond any fixed level of the monadic second-order quantifier alternation hierarchy. (2) On strings with built-in addition, MLFP can describe at least all languages that belong to the linear time complexity class DLIN. (3) Settling the question whether addition-invariant MLFP (?)(=) or, equivalently, settling the question whether MLFP (?)(=) MSO on finite strings with addition would solve open problems in complexity theory: "=" would imply that PH = PTIME whereas "not equal" would imply that DLIN not equal LINH. Apart from this we give a self-contained proof of the previously known result that MLFP is strictly less expressive than MSO on the class of finite graphs. (c) 2005 Elsevier B.V. All rights reserved.