Bounded quantifier

In the study of formal theories in mathematical logic, bounded quantifiers (also known as restricted quantifiers) are often included in a formal language in addition to the standard quantifiers "∀" and "∃". Bounded quantifiers differ from "∀" and "∃" in that bounded quantifiers restrict the range of the quantified variable. The study of bounded quantifiers is motivated by the fact that determining whether a sentence with only bounded quantifiers is true is often not as difficult as determining whether an arbitrary sentence is true.

Examples of bounded quantifiers in the context of real analysis include:

Suppose that L is the language of Peano arithmetic (the language of second-order arithmetic or arithmetic in all finite types would work as well). There are two types of bounded quantifiers: ${\displaystyle \forall n<t}$ and ${\displaystyle \exists n<t}$. These quantifiers bind the number variable n using a numeric term t not containing n but which may have other free variables. ("Numeric terms" here means terms such as "1 + 1", "2", "2 × 3", "m + 3", etc.)

These quantifiers are defined by the following rules (${\displaystyle \phi }$ denotes formulas):

There are several motivations for these quantifiers.

In general, a relation on natural numbers is definable by a bounded formula if and only if it is computable in the linear-time hierarchy, which is defined similarly to the polynomial hierarchy, but with linear time bounds instead of polynomial. Consequently, all predicates definable by a bounded formula are Kalmár elementary, context-sensitive, and primitive recursive.

In the arithmetical hierarchy, an arithmetical formula that contains only bounded quantifiers is called ${\displaystyle \Sigma _{0}^{0}}$, ${\displaystyle \Delta _{0}^{0}}$, and ${\displaystyle \Pi _{0}^{0}}$. The superscript 0 is sometimes omitted.

Suppose that L is the language ${\displaystyle \langle \in ,\ldots ,=\rangle }$ of the Zermelo–Fraenkel set theory, where the ellipsis may be replaced by term-forming operations such as a symbol for the powerset operation. There are two bounded quantifiers: ${\displaystyle \forall x\in t}$ and ${\displaystyle \exists x\in t}$. These quantifiers bind the set variable x and contain a term t which may not mention x but which may have other free variables.