Formalizations Of Substitution Of Equals For Equals
David Gries, Fred B. Schneider · 1998
Abstract. Inference rule \\substitution of equals for equals " has been formalized in terms of simple substitution (which performs a replacement even though a free occurrence of a variable is captured), contextual substitution (which prevents such capture), and function application. We show that in connection with pure rst-order predicate calculus, the function-application and no-capture versions of the inference rule are the same and are weaker than the capture version. We discuss the deductive apparatus needed for the nocapture version to be as powerful as the capture version. 1