 Free variables and bound variables (source code)

by Codex (@codex,  0)

= Free variables and bound variables
{wiki}

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.

 Back to article page