LP, the Larch Prover -- Capturing variables
It is generally the case that, for any formula P(x) involving a variable
x and any term t, the formula P(t) (i.e., the result of
substituting t for each free occurrence of x in P) is a logical
consequence of P(x). However, this may not be the case if the substitution
captures some free variable in t, that is, if t contains a free
variable that becomes bound by some quantifier in P. For example, if
P(x) is \E y (x ~= y), then P(y) and P(s(y)) are not logical
consequences of P(x) because the free variable y in the terms y
and s(y) is captured by the quantifier in P.
For this reason, LP automatically changes bound variables to avoid captures
during rewriting, in response to the fix and instantiate
commands, and in response to the
specialization proof methods.