We can browse some of the "early modern" textbooks :

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$.

$(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 :

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

while in :

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