2
$\begingroup$

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

$\endgroup$
5
$\begingroup$

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

$\endgroup$
  • $\begingroup$ Thanks! Do you know how later literature isolated more recursive definitions? $\endgroup$ – Frode Alfson Bjørdal Feb 8 '15 at 16:58
  • $\begingroup$ 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). $\endgroup$ – Frode Alfson Bjørdal Feb 10 '15 at 3:43
  • $\begingroup$ 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. $\endgroup$ – Frode Alfson Bjørdal Feb 10 '15 at 3:47
  • $\begingroup$ Thanks for the update on February 10. It was the Enderton recursion I was looking for. $\endgroup$ – Frode Alfson Bjørdal Feb 10 '15 at 11:04

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.