Título: Substitution in the Presence of Quantification
Abstract: Aim of this short talk is to outline the formal treatment of substitution in the presence of quantification. For that purpose, we carry over our methods introduced in our last talk from the case of occurrences in usual terms to the realm of untyped lambda calculus. With this formalism available, we are able to define central notions as “free for substitution” and different special substitution functions as the substitution of all free occurrences of a variable or the renaming of bounded variables. We conclude our talk with some remarks about the limits of our methods. In particular, we discuss why we are not able to treat syntactical entities as derivations in the same way.