Bounded quantifier (source code)

= Bounded quantifier

A bounded quantifier has the form $\exists x<t\,\varphi$ or $\forall x<t\,\varphi$, where the term $t$ does not contain $x$. It ranges over a finite initial segment in the standard natural numbers.