Restricted quantifier

A 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 $R(x)$. When used in this restricted sense, the universal quantifier $(\forall x)$ and the 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), where $t$ is a term not containing $x$. When these quantifiers are applied to a decidable predicate, the result is a decidable predicate.