I'll refer to (one of) my preferred textbooks :
he defines substitution by recursion :
- For atomic $\alpha, \alpha_t^x$ is the expression obtained from $\alpha$ by replacing
the variable $x$ by $t$.
- $(∀y \alpha)_t^x$ is $∀y \alpha$, if $x = y$, $∀y(\alpha_t^x)$ if $x \ne y$.
Then he discuss the fallacy of substituting $y$ for $x$ into $∀x¬∀y(x=y)$, getting the wrong : $¬∀y(y=y)$, which again is exactly your example.
The problem is that when $y$ was substituted for $x$, it was immediately “captured” by the $∀y$ quantifier. We must impose a restriction [...] that will preclude this sort of quantifier capture. Informally, we can say that a term $t$ is not substitutable for $x$ in $\alpha$ if there is some variable $y$ in $t$ that is captured by a $∀y$ quantifier in $\alpha_t^x$.
Thus [page 113] he defines :
Let $x$ be a variable, $t$ a term. We define the phrase “$t$ is substitutable for $x$ in $\alpha$” as follows:
- For atomic $\alpha, t$ is always substitutable for $x$ in $\alpha$. (There are no
quantifiers in $\alpha$, so no capture could occur.)
- $t$ is substitutable for $x$ in $∀y\alpha$ iff either
(a) $x$ does not occur free in $∀y\alpha$, or
(b) $y$ does not occur in $t$ and $t$ is substitutable for $x$ in $\alpha$. (The point here is to be sure that nothing in $t$ will be captured by the $∀y$ prefix and that nothing has gone wrong inside $\alpha$ earlier.)
For example, $x$ is always substitutable for itself in any formula. If $t$ contains no variables that occur in $\alpha$, then $t$ is substitutable for $x$ in $\alpha$.
The reader is cautioned not to be confused about the choice of words. Even if $t$ is not substitutable for $x$ in $\alpha$, still $\alpha_t^x$ is obtained from $\alpha$ by
replacing $x$ wherever it occurs free by $t$.
The two definitions are exactly the same as in Christopher Leary, A Friendly Introduction to Mathematical Logic (2000), pages 39-41.
I think that you are "not seeing" the difference between the two concepts because you are thinking only to one part of the problem :
$(∀y \alpha)_t^x$ is $∀y \alpha$, if $x = y$, $∀y(\alpha_t^x)$ if $x \ne y$.
This clause prevent us from replacing the bound variable. I.e. with $∀y(x=y)$ we can perform $(∀y(x=y))_t^x$ to get $∀y(t=y)$ but we cannot perform $(∀y(x=y))_t^y$.
But we have another possible (bad) case : when $t$ has free variables inside, included the "degenerate" case when $t$ is $y$.
In this case the above clause tells us nothing, because we are trying to put $t$ (i.e. $y$) in place of $x$ inside $∀y(x=y)$. In this case $x$ is not the bound variable (which is $y$) but the result is still not what we expect.
The formula :
is true in a model with only one object, while :
is true in every model.