Substituting terms in place of variables inside formulas My reference is "A Course on Mathematical Logic" by S.M. Srivastava. I have trouble understanding some points in this remarkable book.

Substituting a term in place of a variable in a formula. Why is substitution defined as it is?

This is in the context of first order logic. Take a language $L$ (variables, constant symbols, function symbols, relation symbols (among which $=$), logical connectives ($ \neg,\vee)$ and the existential quantifier ($\exists$)). We are given a term $t=t[v_1,\dots,v_n]$ and a formula $\varphi=\varphi[x_1,\dots,x_m]$. This notation means that the variables that figure in $t$ are among $\lbrace v_1,\dots,v_n \rbrace$, and the free variables in $\varphi$ are among $\lbrace x_1,\dots,x_m \rbrace$. 
The author defines that $t$ is substitutiable in place of a variable $x$ in $\varphi$, if for every variable $v$ effectively occurring in $t$ (thus $v\in\lbrace v_1,\dots,v_n \rbrace$), and every subformula $\exists v \psi$ of $\varphi$, if $x$ occurs in this subformula, it is not free (considered as an occurrence inside $\varphi$). If $t$ is substitutiable for $x$ in $\varphi$, you define $\varphi_x[t]$ to be the formula in which every free occurrence of $x$ in $\varphi$ has been replaced by the term $t$.
For instance, take $\varphi=\varphi[x,y]$ to be $\neg (x=0) \vee \exists x (x=y)$ in a language with a constant symbol $0$. Suppose there is a $1$-ary function symbol $f$ and define $t=f(x)$. By definition, $t$ is substitutiable for $x$ in $\varphi$. Indeed, there is only one subformula of the form $\exists x\psi$ in $\varphi$, and in it, the occurrences of $x$ are all bounded. If we go to replace $t$ in $\varphi$ everywhere $x$ is free, we get $$ \varphi_x[t]= \neg (t=0) \vee \exists x (x=y)=\neg (f(x)=0) \vee \exists x (x=y)$$
On the other hand, $t$ is not substitutiable for $y$ because $y$ occurs in the term $\exists x(x=y)$ but is free as an occurrence in $\varphi$. The $\neg(x=0)$ part of the forumla I only included so as to have a free occurrence of $x$ where actual substitution could be seen.
For simplicity, change $\varphi$ to be $\exists x(x=y)$, again, $t$ may not be substituted in place of $y$ inside $\varphi$. I intuitively understand that simply replacing $y$ with $t$ would give a formula that is qualitatively different from $\varphi$ : $\exists x (x=f(x))$ is a very different matter than $\exists x(x=y)$ or $\exists x(x=f(z))=\varphi_y[f(z)]$

Can someone explain that 'intuition' and justify why Srivastava's definition is indeed the correct definition?

 A: The variables in $t$ are intended to be free variables. As far as they coincide with free variables in $\varphi$, they're intended to refer to those variables. That if $x$ occurs under the scope of a quantifier with dummy variable $v$ it is not free means that there are no free occurrences of $x$ under the scope of quantifiers with dummy variable $v$, which means that $t$ will not be substituted under the scope of any quantifier with dummy variable $v$, which means that $t$'s variable $v$ will not come under the scope of any quantifier, which it mustn't, since its intended meaning is a free variable.
This sort of thing becomes much simpler if you first rename all dummy variables to be distinct from all free variables; then you don't need this sort of restriction. Another way of looking at it is to say that $t$ is substitutable (no 'i' there usually, does Srivastava spell it with an 'i'?) into $\varphi$ iff the result can be transformed by renaming dummy variables into the result of first making all dummy variables distinct and then substituting.
