(1) The condition that a term $a$ be substitutable for another term in an expression can be given a recursive definition. Who first developed such a definition?


(2) One sometimes see the phrase "$a$ is free for $u$ in E" used with the same meaning as "$a$ is substitutable for $u$ in E"; where does this language use stem from?



Two questions on substitutability
We can browse some of the "early modern" textbooks :


* Stephen Cole Kleene, [Introduction to Metamathematics](https://books.google.it/books?id=HZAjPwAACAAJ) (1952), page 79 :



> 
> we say that a term $t$ is *free at the free occurrences of* a variable $x$ *in* a formula $A(x)$ (or $t$ is *free at the substitution positions for* $x$ *in* $A(x)$, or briefly $t$ is *free for* $x$ *in* $A(x)$), if no free occurrence of $x$ in $A(x)$ is in the scope of a quantifier $\forall y$ or $\exists y$ where $y$ is a variable of $t$.
> 
> 
> 


* Alonzo Church, [Introduction to Mathematical Logic](https://books.google.it/books?id=JDLQOMKbdScC&pg=PA172) (1956), page 172 :



> 
> $(a)A \supset S^a\_bA|$, where $a$ is an individual variable, $b$ is an individual variable or individual constant and no free occurrence of $a$ in $A$ is in a wf part of $A$ of the form $(b)C$.
> 
> 
> 


* Joseph Shoenfield, Mathematical Logic (1967), page 17 :



> 
> We say that [a term] $a$ is *substitutible* for $x$ in $A$ if for each variable $y$ occurring in $a$, no part of $A$ of the form $\exists yB$ contains an occurrence of $x$ which is free in $A$.
> 
> 
> 


*Note*


I think that the focus of Church and Kleene to the details of *substitution* dates back to Church's (failed) attempt to develop the symbolism of formal logic "without free variables" [see A.Church, [A Set of Postulates for the Foundation of Logic](http://www.jstor.org/discover/10.2307/1968337?sid=21105814183713&uid=378508341&uid=2&uid=70&uid=2134&uid=378508351&uid=3738296&uid=3&uid=60), *Annals of Mathematics*, Second Series, Vol. 33, No. 2 (Apr., 1932), pp. 346-366; and see page 350 for an early occurrence of the substitution operator : $S^X\_YU|$].


This attempt produced the $\lambda$-calculus; see Alonzo Church, [The Calculi of Lambda-conversion](https://books.google.it/books?id=KCOuGztKVgcC&printsec=frontcover) (1941).




---


An "early" inductive definition is in :


* Raymond Smullyan, [First-Order Logic](https://books.google.it/books?id=kgvhQ-oSZiUC&pg=PA44) (1968), page 44 [note that Smullyan uses in the first-order langauge the "device" - due to Gentzen - of separating *individual variables* : $x,y,z$ (to be used bound) from *individual parameters* : $a,b$ (to be used free)] :



> 
> For every formula $A$, variable $x$ and parameter $a$, we define the formula $A^x\_a$ by the following inductive schema :
> 
> 
> 
> > 
> > (1) if $A$ ia *atomic*, then $A^x\_a$ is the result of substituting $a$ for every occurrence of $x$ in $A$.
> > 
> > 
> > (2) $[A \land B]^x\_a= A^x\_a \land B^x\_a$
> > 
> > 
> > 
> 
> 
> 


[...]



> 
> 
> > 
> > (3) $[(\forall x)A]^x\_a=(\forall x)A$.
> > 
> > 
> > 
> 
> 
> But for a variable $y$ distinct from $x$
> 
> 
> 
> > 
> > $[(\forall x)A]^y\_a=(\forall x)[A^y\_a]$.
> > 
> > 
> > 
> 
> 
> 




---


We can find into :


* Herbert Enderton, [A Mathematical Introduction to Logic](https://books.google.it/books?id=dVncCl_EtUkC&pg=PA113) (2nd ed - 2001), page 113, the definition by recursion of :



> 
> the phrase “$t$ is substitutable for $x$ in $\alpha$”,
> 
> 
> 


while in :


* Elliott Mendelson, [Introduction to mathematical logic](https://books.google.it/books?id=ZO1p4QGspoYC&pg=PA54) (4th ed - 1997), page 54, we have the "traditional" definition of :



> 
> [what is said for ] a *term* $t$ to be *free for* $x\_i$ *in* $\mathcal B$.
> 
> 
> 


