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?