The standard translation of existential fixed-point formulas into second-order logic produces strict universal formulas, that is, formulas consisting of universal quantifiers on relations (not functions) followed by an existential first-order formula. This form implies many of the pleasant properties of existential fixed-point logic, but not all. In particular, strict universal sentences can express some co-NP-complete properties of structures, whereas properties expressible by existential fixed-point formulas are always in P. We therefore investigate what additional syntactic properties, beyond strict universality, are enjoyed by the second-order translations of existential fixed-point formulas. In particular, do such syntactic properties account for polynomial-time model-checking?
Blass, A. (2015). Existential fixed-point logic as a fragment of second-order logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9300, pp. 52–68). Springer Verlag. https://doi.org/10.1007/978-3-319-23534-9_3