View source for Restricted quantifier

{{TEX|done}}
A [[Quantifier|quantifier]] applied to predicates not with respect to the whole range of a given object variable, but with respect to a part of it defined by a [[Predicate|predicate]] $R(x)$. When used in this restricted sense, the [[Universal quantifier|universal quantifier]] $(\forall x)$ and the [[Existential quantifier|existential quantifier]] $(\exists x)$ are usually denoted by $(\forall x)_R(x)$ and $(\exists x)_R(x)$ (or $\forall x\colon R(x)$ and $\exists x\colon R(x)$, respectively). If $P(x)$ is a predicate, then $(\forall x)_R(x)P(x)$ means

$$\forall x(R(x)\supset P(x)),$$

that is, the predicate $P(x)$ is true for all values of the variable $x$ satisfying the predicate $R(x)$. The proposition $(\exists x)_R(X)P(x)$ means

$$\exists x(R(x)\&P(x)),$$

that is, the intersection of the truth domains of the predicates $R(x)$ and $P(x)$ is non-empty.

Restricted quantifiers of the form $(\forall x)_{x<t}$ and $(\exists x)_{x<t}$ (more commonly called bounded quantifiers) play an important role in formal arithmetic (cf. [[Arithmetic, formal|Arithmetic, formal]]), where $t$ is a term not containing $x$. When these quantifiers are applied to a [[Decidable predicate|decidable predicate]], the result is a decidable predicate.