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\)). e. by counting alternations of bounded quantifiers, ignoring sharply bounded ones. The theories \(\mathsf{S}^i_2\) and \(\mathsf{T}^i_2\) both extend a base theory known as \(\textsf{BASIC}\). , Hájek and Pudlák 1998