= Variable capture
An unintended change of binding caused by moving or substituting a term beneath a binder. In <first-order logic>, substituting $y$ for the free $x$ in $\forall y\,S(x,y)$ without renaming would yield $\forall y\,S(y,y)$, incorrectly binding the substituted occurrence. First rename the bound $y$ to a fresh $z$, obtaining $\forall z\,S(x,z)$, and then substitute to get $\forall z\,S(y,z)$. The paper's condition that a term be free for a variable excludes such capture.
Back to article page
