# 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?

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

• Thanks! Do you know how later literature isolated more recursive definitions? – Frode Alfson Bjørdal Feb 8 '15 at 16:58
• Thanks again for more information. That Church was unto this does not come as a surprise to me, as I belong to the elite that took a graduate seminary in logic from him at UCLA and also read his 1941 monography. There is a better recursive definition which I can reproduce at request or in PM, and I have the suspicion that it was in Shoenfield's book (which I at least used to own). – Frode Alfson Bjørdal Feb 10 '15 at 3:43
• Thanks also for the reference to the Smullyan book where he makes the said formal distinction in syntax between bound and free variables; I didn't know. – Frode Alfson Bjørdal Feb 10 '15 at 3:47
• Thanks for the update on February 10. It was the Enderton recursion I was looking for. – Frode Alfson Bjørdal Feb 10 '15 at 11:04