INFINITARY LOGIC AND INDUCTIVE DEFINABILITY OVER FINITE STRUCTURES

The extensions of first-order logic with a least fixed point operator (FO + LFP) and with a partial fixed point operator (FO + PFP) are know n to capture the complexity classes P and PSPACE respectively in the p resence of an ordering relation over finite structures. Recently, Abit eboul and Vianu (in ''Proceedings of the 23rd ACM Symposium on the The ory of Computing,'' 1991) investigated the relationship of these two l ogics in the absence of an ordering, using a machine model of generic computation. In particular, they showed that the two languages have eq uivalent expressive power if and only if P = PSPACE. These languages c an also be seen as fragments of an infinitary logic where each formula has a bounded number of variables, L(infinity w)(w), (see, for instan ce, Kolaitis and Vardi, in ''Proceedings of the 5th IEEE Symposium on Logic in Computer Science,'' pp. 156-167, 1990). We investigate this l ogic on finite structures and provide a normal form for it. We also pr esent a treatment of Abiteboul and Vianu's results from this point of view. In particular, we show that we can write a formula of FO + LFP t hat defines an ordering of the L(infinity w)(k), 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 o f structures where every element is definable. We also settle a conjec ture mentioned by Abiteboul and Vianu by showing that FO + LFP is prop erly contained in the polynomial time computable fragment of L(infinit y w)(w), raising the question of whether the latter fragment is a recu rsively enumerable class. (C) 1995 Academic Press, Inc.