I am studying formal proofs of first order logic, in particular the meta-theorem of generalisation:
Generalisation: $\Gamma \vdash \phi$ and $x$ does not occur free in any formula of $\Gamma$ then $\Gamma \vdash \forall x \phi$
My question is about the side condition: I understand some simple counterexamples which show that the rule is unsound without the side condition. But I have questions about theories with axiom schemata, for example the induction axiom in Peano arithmetic (PA):
If an axiom schema allows an instantiation with free variable $x$, does that mean the generalisation rule cannot be applied to $x$?
In particular in PA, is there a restriction that the induction axiom can only be instantiated with formulae that have only the "induction variable" as free variable?