Fixpoint logic vs. infinitary logic in finite-model theory

The relationship between fixpoint logic and the infinitary logic L_∞ω^ω with a finite number of variables is studied. It is observed that the equivalence of two finite structures with respect to L_∞ω^ω is expressible in fixpoint logic. As a first application of this, a normal-form theorem for L∞_ω^ω on finite structures is obtained. The relative expressive power of first-order logic, fixpoint logic, and L_∞ω^ω on arbitrary classes of finite structures is examined. A characterization of when L_∞ω^ω collapses to first-order logic on an arbitrary class of finite structures is given