On the expressive power of variable-confined logics

In this paper we study the comparative expressive power of variable-confined logics, that is, logics with a fixed finite number of variables. This is motivated by the fact that the number of variables is considered a logical resource in descriptive complexity theory. We consider the expressive power of the logics FO^k (first-order logic with k variables), LFP^k (LFP with k variables, appropriately defined), and L_∞w^k (infinitary logic with k variables) over classes of finite structures. While the definitions of FO^k and L_∞w ^k are quite clear, it turns out that ramifying LFP is a more delicate matter. We define LFP^k in terms of systems of least fixpoints, i.e., instead of taking the least fixpoint of a single positive first-order formula, we consider simultaneous least fixpoints of a vector of positive first-order formulas. As evidence that LFP^k , k⩾1, is the right ramification of LFP we offer two main results. The first is a new proof of a theorem by A. Dawar et al. (1995) to the effect that equivalence classes of finite structures with respect to the logic L_∞w^k are expressible in FO ^k. The second result, novel and technically difficult, is a characterization for each k⩾1 of the collapse of L_∞w ^k to FO^k in terms of boundedness of LFP^k. More precisely, we establish the following stronger version of McColm´s second conjecture: L_∞w^k =FO^k on a class C of finite structures if and only if LFP^k is uniformly bounded on C