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