Bounded quantifier

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

• ${\displaystyle \forall x>0}$ - for all x where x is larger than 0
• ${\displaystyle \exists y<0}$ - there exists a y where y is less than 0
• ${\displaystyle \forall x\in \mathbb {R} }$ - for all x where x is a real number
• ${\displaystyle \forall x>0\quad \exists y<0\quad (x=y^{2})}$ - every positive number is the square of a negative number

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 and contain a numeric term t which may not mention 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):

${\displaystyle \exists n<t\,\phi \Leftrightarrow \exists n(n<t\land \phi )}$

${\displaystyle \forall n<t\,\phi \Leftrightarrow \forall n(n<t\rightarrow \phi )}$

There are several motivations for these quantifiers.

• In applications of the language to recursion theory, such as the arithmetical hierarchy, bounded quantifiers add no complexity. If ${\displaystyle \phi }$ is a decidable predicate then ${\displaystyle \exists n<t\,\phi }$ and ${\displaystyle \forall n<t\,\phi }$ are decidable as well.
• In applications to the study of Peano arithmetic, the fact that a particular set can be defined with only bounded quantifiers can have consequences for the computability of the set. For example, there is a definition of primality using only bounded quantifiers: a number n is prime if and only if there are not two numbers strictly less than n whose product is n. There is no quantifier-free definition of primality in the language ${\displaystyle \langle 0,1,+,\times ,<,=\rangle }$, however. The fact that there is a bounded quantifier formula defining primality shows that the primality of each number can be computably decided.

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.

The semantics of these quantifiers is determined by the following rules:

${\displaystyle \exists x\in t\ (\phi )\Leftrightarrow \exists x(x\in t\land \phi )}$

${\displaystyle \forall x\in t\ (\phi )\Leftrightarrow \forall x(x\in t\rightarrow \phi )}$

A ZF formula that contains only bounded quantifiers is called ${\displaystyle \Sigma _{0}}$, ${\displaystyle \Delta _{0}}$, and ${\displaystyle \Pi _{0}}$. This forms the basis of the Lévy hierarchy, which is defined analogously with the arithmetical hierarchy.

Bounded quantifiers are important in Kripke–Platek set theory and constructive set theory, where only Δ₀ separation is included. That is, it includes separation for formulas with only bounded quantifiers, but not separation for other formulas. In KP the motivation is the fact that whether a set x satisfies a bounded quantifier formula only depends on the collection of sets that are close in rank to x (as the powerset operation can only be applied finitely many times to form a term). In constructive set theory, it is motivated on predicative grounds.

• Subtyping — bounded quantification in type theory
• System F_<: — a polymorphic typed lambda calculus with bounded quantification

• Hinman, P. (2005). Fundamentals of Mathematical Logic. A K Peters. ISBN 1-56881-262-0.
• Kunen, K. (1980). Set theory: An introduction to independence proofs. Elsevier. ISBN 0-444-86839-9.