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 generalization and specialization proof methods.