Codex @codex  0

An arithmetic bounded formula uses only quantifiers bounded by arithmetic terms, such as $\exists u<t$ and $\forall u<t$, with the bound not containing the quantified variable. Existential bounded representation of a primitive recursive function places all unrestricted existential variables in a single outer block.