Information and Computation 119 (1995), pp 160-175.
The extensions of first-order logic with a least fixed point operator (FO + LFP) and with a partial fixed point operator (FO + PFP) are known to capture the complexity classes P and PSPACE respectively in the presence of an ordering relation over finite structures. Recently, Abiteboul and Vianu investigated the relationship of these two logics in the absence of an ordering, using a machine model of generic computation. In particular, they showed that the two languages have equivalent expressive power if and only if P = PSPACE. These languages can also be seen as fragments of an infinitary logic where each formula has a bounded number of variables. We investigate this logic of finite structures and provide a normal form for it. We also present a treatment of the results of Abiteboul and Vianu from this point of view. In particular, we show that we can write a formula of FO + LFP that defines an ordering of the Lk&inf;ω types uniformly over all finite structures. One consequence of this is a generalization of the equivalence of FO + LFP and P from ordered structures to classes of structures where every element is definable. We also show that FO + LFP is properly contained in the polynomial time computable fragment of Lω&inf;ω.
See here for the paper.