I'm reading Leary's Mathematical Logic text where it defines the phrase "substitutable" and most of it is sensible:
$t$ is substitutable for $x$ in $\phi$ if
$\phi$ is atomic.
$\phi := \neg \alpha$ and $t$ is substitutable for $x$ in $\alpha$.
$\phi := \alpha \lor \beta$ and $t$ is substitutable for $x$ in both $\alpha$ and $\beta$.
$\phi := (\forall y)\alpha$ and either
a. $x$ is not free in $\phi$ or
b. $y$ does not occur in $t$ and $t$ substitutable for $x$ in $\alpha$.
All of this except 4.a. makes sense to me, but why would you want $x$ not free in $\phi$? I mean you could have $\phi = (\forall x)(Px)$ so that $x$ is not free in $\phi$ but you would think this is the precise case where you don't want to say that $t$ is substitutable for $x$, right? (Here I take $x=y$, and it is common for Leary to use variables to possibly take as a value other variables.)
From the material earlier in the book I don't think the intention here is to say that, in such a case, $\phi_t^x = (\forall t)(Pt)$ because, for one thing, this is not what follows from the definition of substitution given earlier and for another thing he is trying to allow for $t$ to be functions of terms---and nowhere in the book does he write something like $(\forall f(c))(P(f(c))$.
I don't have the book, but this must go with a definition of substitution of $t$ for $x$ in $\phi$, which I'd write $\phi[t/x]$ and which you are writing as $\phi^x_t$. The definition goes like this (where $y$ denotes any variable other than $x$): $$ \begin{array}{tcl} x[t/x] & = & t \\ y[t/x] & = & y \\ (\lnot\alpha)[t/x] & = & \lnot(\alpha [t/x]) \\ (\alpha \lor \beta)[t/x] & = & \alpha[t/x] \lor \beta[t/x] \\ ((\forall x) \alpha)[t/x] & = & (\forall x) \alpha \\ ((\forall y) \alpha) [t/x] & = & (\forall y) (\alpha[t/x]) \end{array} $$
However, the last clause is not always semantically acceptable. To see what can go wrong, consider the formula $(\forall x)\lnot((\forall y)y + 1 \le x)$. This formula is true and we want to be able to deduce consequences of it by instantiating the bound variable $x$. I.e., given any term $t$, we should have that $\lnot((\forall y) y + 1 \le x)[t/x]$. But if $y$ appears free in $t$, this breaks down: if we just do the substitution according to the above definition with $t \equiv y + 1$, we get the false statement $\lnot((\forall y) y + 1 \le y + 1)$. This has gone wrong because $t$ is not substitutable for $x$ in $(\forall y) y + 1 \le x$ and doing the substitution has invalidly identified the outside world's $y$ with the bound $y$ inside $\forall y\, y + 1 \le x$. To do the substitution validly, we need to rename the bound variable $y$ in $\lnot((\forall y) y + 1 \le x)[t + 1/x]$ to give the equivalent formula $\lnot((\forall z) z + 1 \le x)[t + 1/x]$ and then we get the valid statement $\lnot((\forall z) z + 1 \le y + 1)$.
It would be more intuitive to say validly substitutable rather than substitutable, because substitutable read informally does suggest that it's OK just to replace all the $x$s by $t$s. You have to read it in the context of a definition of substitution for $x$ that always treats bound occurrences of $x$ correctly (by leaving them alone) but only sometimes treats bound occurrences of other variables correctly.