1. A variable referred to in a function, which is not an argument of the function. In lambda-calculus, x is a bound variable in the term M = \ x . T, and a free variable of T. We say x is bound in M and free in T. If T contains a subterm \ x . U then x is rebound in this term. This nested, inner binding of x is said to "shadow" the outer binding. Occurrences of x in U are free occurrences of the new x.
Variables bound at the top level of a program are technically free variables within the terms to which they are bound but are often treated specially because they can be compiled as fixed addresses. Similarly, an identifier bound to a recursive function is also technically a free variable within its own body but is treated specially.
A closed term is one containing no free variables.
See also closure, lambda lifting, scope.
2. In predicate logic, an individual variable at least one of whose occurrences in a wff does not lie within the scope of a quantifier on the same letter. Because other occurrences may be bound, a variable may be both free and bound in the same wff.
3. free occurrence of a variable
Any occurrence of an individual variable not within the scope of a quantifier on the same letter.
See bound variable, closure
[Glossary of First-Order Logic]
Try this search on OneLook / Google