Bounded arithmetic formulas

Work in first-order arithmetic over $\mathbb{N}$. A quantifier is bounded when it has the form $\mathrm{\exists }u<t(\vec{x})$ or $\mathrm{\forall }u<t(\vec{x})$, where $t$ is an arithmetic term. A formula is bounded when every one of its quantifiers is bounded.

For the normal-form presentation of the arithmetical hierarchy on this page, we also permit an arbitrary primitive-recursive predicate $R(\vec{x})$ in the sense of Primitive recursive functions as the quantifier-free matrix. This is an additional presentation convention: it does not assert that every primitive-recursive predicate is definable by a bounded formula in the bare first-order language chosen above.

Unbounded quantifiers are the displayed leading quantifiers used to measure an arithmetical level; bounded quantifiers do not contribute an alternation.