Partial Fixed Point for Finite Models in Second Order Logic

We investigate second order (SO) logic with partial fixed point (PFP) operators for finite models. It is known that PFP-logic corresponds to PSPACE, and SO-logic for finite structures corresponds to the union of polynomial hierarchy. We propose an explicit algorithm for translation first order (FO) logic with PFP-operators to FO-logic with only one PFP-operator for finite models with linear order. Next we generalize this result to SO-logic.