Give a deduction of $\forall zP(z)$ from $\forall xP(x)$. I am to give a deduction of the formula $\forall zP(z)$ from the given $\forall xP(x)$. So far I know that, because $x$ is always substitutable for itself, I have $P(x)$. My next step I think is to substitute $z$ for $x$ to get $P(z)$. However, I'm not sure how to proceed from here, or even if I'm allowed to substitute $z$ for $x$. A hint would be greatly appreciated. Thanks.
 A: From the first quantifier rule, $(\forall x)P(x) \to P(z)$ entails that $(\forall x)P(x) \to (\forall z)P(z)$ (taking $\psi$ to be $(\forall x)P(x)$). But $(\forall x)P(x) \to P(z)$ is instantiation (note that the notation $\varphi^x_t$ means ``$\varphi$ with $x$ replaced with a term $t$'', and $z$ is a term).
This is made slightly fishy by the fact that the rules as you stated them only allow you to deduce $(\forall x)P(z)$, not $(\forall z)P(z)$; I suspect it says somewhere that in the quantifier rules, any variable may be used in place of $x$ in the quantifiers.
A: From the first quantifier axiom : 

$(∀xϕ)→ϕ^x_t$

we can derive the instance: $(∀xP(x))→P(z)$.
What about the proviso that $z$ must be substitutable for $x$ in $P(x)$ ?
It is obviously satisfied, because $P(x)$ is not a schema, like $ϕ$: $P(x)$ is a unary predicate letter, with only one argument place. Thus, there are no "hidden" quantifiers that can "capture" $z$.
Now you can apply the first quantifier rule.
There are no free variables in  $(∀xP(x))$ and thus the proviso of the quantifier rule: "whenever $x$ is not free in $\psi$ ....", is satisfied with every variable, including $z$. 
