Two questions on substitutability (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?
 A: We can browse some of the "early modern" textbooks :


*

*Stephen Cole Kleene, Introduction to Metamathematics (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 (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, 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 (1941).

An "early" inductive definition is in :


*

*Raymond Smullyan, First-Order Logic (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 (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 (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$.

