A variable occurrence is bound when it falls within the scope of a binding operation that binds that occurrence; otherwise it is free. Quantifiers and lambda abstractions are common binders. In first-order formulas, a free variable occurrence is outside the scope of a corresponding quantifier.
Articles by others on the same topic
In the context of formal logic, mathematics, and computer science, the concepts of **free variables** and **bound variables** are important in understanding the structure of expressions, particularly in terms of quantification and function definitions. ### Free Variables A **free variable** is a variable that is not bound by a quantifier or by the scope of a function. In simpler terms, free variables are those that are not limited to a specific context or definition, meaning they can represent any value.