Free variable

free occurrence of a variable

The occurrence of a variable in a linguistic expression as a parameter of this expression. A rigorous definition of this concept can be given only for a formalized language. Every language has its own definition of a free variable, depending on the rules for forming expressions in the particular language. The semantic criterion is the following condition: The substitution of any object from an implicit interpretation in place of the given occurrence(s) of a variable must not lead to an absurd expression. For example, in the expression , which denotes the set of points of a circle of radius , the variable is free while and are not (see Bound variable). If denotes a mapping of the form , and the variables and range over and , respectively, then in the expression the variables and are free (and so is , if it is considered as a variable with respect to functions). For a fixed and by varying one obtains a function of the form , which is denoted by . In this expression is free and is not. In the expression , which denotes the value of the function at an arbitrary point , the last occurrence of is free while the two others are not. The first occurrence is called an operator occurrence (it is under the sign of an operator), and the second a bound occurrence.

For a non-formalized language, that is, in actual mathematical texts, for an individual expression it is not always possible to definitely identify the free variables and the bound ones. For example, in , depending on the context, the variable can be free and bound, or vice-versa, but they cannot both be free. An indication of which variable is assumed to be free is given by using additional means. For example, if this expression is met in a context of the form "let fk=i< kaik" , then is free. If there is agreement that there is no summation over , then is a parameter. The expression , often used in mathematics, sometimes denotes a one-element set, in which case the variable occurs freely, and sometimes denotes the set of all where runs over an assigned domain of objects, in which case is a bound variable.

References

[a1]	S.C. Kleene, "Introduction to metamathematics" , North-Holland (1951)