Bound variable

bound occurrence of a variable

A type of occurrence of a variable in a linguistic expression. An exact definition for each formalized language depends on the rules of formation of the language. It is not possible to substitute objects in place of a bound variable, since such a substitution would lead to meaningless expressions. But the replacement of a bound variable, where it occurs, by a new (for a given expression) variable leads to an expression with the same meaning. For example, in the expressions $$ \int f(x,y)\,d x\,,\ \ \ \{ x : f(x,y) = 0 \}\,, $$ $x$ is a bound variable. Replacing $x$ by a number leads to a meaningless expression, whereas by writing $z$ everywhere instead of $z$ one obtains an expression with exactly the same meaning.

Bound variables always arise in applying to an expression $\mathcal{E}$ with free occurrences of a variable $x$ an operator variable $x$ (see Free variable). In the resulting expression, all the occurrences of $x$ in $\mathcal{E}$ that were previously free become bound. We mention below certain operators that are often used (next to the operators $\int \ldots dx$ and $\{ x : \ldots \}$), in which $x$ is an operator variable:

$\forall x (\ldots)$, $\exists x (\ldots)$, that is, the universal and existential quantifiers;

$\int_{\ldots}^{\ldots} \ldots dx$, that is, a definite integral with respect to $x$;

$\sum_x$ that is, summation over $x$;

$\lambda x . (\ldots)$, that is, a function of $x$ the value of which at $x$ is $\ldots$. Specific linguistic expressions can be substituted in place of the dots.

In real (non-formalized) mathematical texts it is possible to have a non-unique use for one and the same expression; in this connection distinguishing a bound variable in a given expression depends on the context and meaning of the expression. In formalized languages there is a formal procedure for distinguishing free and bound occurrences of variables.