 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 yS(x,y)$ without renaming would yield $\forall yS(y,y)$, incorrectly binding the substituted occurrence. First rename the bound $y$ to a fresh $z$, obtaining $\forall zS(x,z)$, and then substitute to get $\forall zS(y,z)$. The paper's condition that a term be free for a variable excludes such capture.