 Hierarchies based on quantifier structure are a useful method to compare the definability of concepts in different systems. In first order logic it was observed very early on that formulas can be brought into a logically equivalent Prenex Normal Form in which all quantifiers occur in the beginning of the formula. This is possible also in second-order logic and the proof is essentially the same. Moreover, using the equivalence (which is reminiscent of a principle of set theory called Axiom of Choice, to which we return in Section 5.4., since in the below formula the relation \(Y\) in a sense chooses one \(X\) for each \(x\) and puts them together into one relation \(Y\) – see entry on  Axiom of Choice  for more on the topic.)