Characterizing Second Order Logic with First Order Quantifiers
David Harel · Mathematical logic quarterly · 1979
A language Q is defined and given semantics, the formulae of which are quantifier-free first-order matrices prefixed by combinations of finite partially ordered first-order quantifiers. It is shown that Q is equivalent in expressive power to second order logic by establishing the equivalence of alternating second order quantifiers and forming conjunctions of partially ordered first-order quantifiers.