Bound variable

A variable occurrence is bound when it lies within the scope of a quantifier that governs it. Its value is determined by that quantifier rather than by an assignment to a free variable.

Quantifier: A symbol or expression that specifies how many objects in a domain satisfy a condition. A quantifier creates the scope in which its variable occurrences can be bound.
Universal quantification: A quantification asserting that a formula holds for every object in a domain. In ∀x P(x), the quantifier binds the occurrences of x in its scope.
Assignment function: A mapping from variables to objects in a model’s domain. Assignments supply values for free variables, while quantifiers vary values for bound ones.
Substitution (logic): Replacing variable occurrences in a logical expression with terms according to specified rules. Correct substitution must distinguish occurrences governed by binders from free ones.
Scope (logic): The portion of a logical expression governed by an operator or quantifier. An occurrence is bound only when it lies inside the governing quantifier’s scope.
Existential quantification: A quantification asserting that a formula holds for at least one object in a domain. In ∃x P(x), the quantifier binds the occurrences of x in its scope.
Closed formula: A formula with no free variable occurrences. A formula is closed when every variable occurrence is bound.
First-order semantics: The interpretation of first-order languages using domains, relations, and variable assignments. Its satisfaction clauses explain how quantifiers evaluate formulas containing bound variables.
Free variable: A variable occurrence not governed by a quantifier or other binder within its expression. Free occurrences depend on an external assignment, unlike bound occurrences.
Variable capture: An unintended change in variable binding caused by substituting an expression into a formula. Substitution can turn a formerly free occurrence into one captured by a quantifier.

Linked from 11 pages