 The collection \(\Delta_0\) of arithmetical formulas in which all quantifiers are bounded is the lowest level of a classical arithmetical hierarchy based on the pattern of alternations of quantifiers in a prenex formula. In \(\mathbf{HA}\) not every formula has a prenex form, but Burr [2004] discovered a simple intuitionistic arithmetical hierarchy corresponding level by level to the classical. For the purposes of the next two definitions only, \(\forall x\) denotes a block of finitely many universal number quantifiers, and similarly \(\exists x\) denotes a block of finitely many existential number quantifiers. With these conventions, Burr’s classes \(\Phi_n\) and \(\Psi_n\) are defined by: