whose provably total functions correspond to the levels of the hierarchy \(\Box^P_i\). These theories are stated over the language \(\mathcal{L}^b_a = \{0,s,+,x,\lt,\lvert \cdot\rvert,\lfloor \frac{x}{2} \rfloor, \#\}\), where the intended interpretation of \(\lvert x\rvert\) is \(\lceil \log_2(x+1) \rceil\), and of \(x\#y\) is \(2^{\lvert x\rvert \cdot \lvert y\rvert}\) as above. Whereas a traditional bounded quantifier is of the form \(\forall x \lt t\) or \(\exists x \lt t\), a so-called sharply bounded quantifier is of the form \(\forall x \lt \lvert t\rvert\) or \(\exists x \lt \lvert t\rvert\) (for \(t\) an \(\mathcal{L}^b_a\)-term not involving \(x\)). The syntactic classes \(\Sigma^b_i\) and \(\Pi^b_i\) are defined in a manner reminiscent to how the classes \(\Sigma^0_i\) and \(\Pi^0_i\) are defined in the traditional arithmetical hierarchy – i.e. by counting alternations of bounded quantifiers, ignoring sharply bounded ones.