In many places, I see the definition for universal generalisation given as follows:
If $\Gamma \vdash \phi$, then $\Gamma \vdash \forall x \phi[x/t]$, as long as the term $t$ is not contained within any formulas within $\Gamma$.
However, I often see this deduction, which seems perfectly valid but does not fit the general form of this rule:
$$P(a) \to P(a) \vdash \forall a(P(a) \to P(a))$$
That is, no substitution as such occurs, unless you consider it a 'degenerate' substitution, where $x$ and $t$ are the same term.
Therefore, if I'm being pedantic, the above definition of UG is unsuitable, we would need to also supplement it with:
If $\Gamma \vdash \phi$, then $\Gamma \vdash \forall x \phi$, as long as the term $x$ is not contained within any formulas within $\Gamma$.
Would this be correct? Or does the first definition implicitly allow the 'degenerate' case $\phi[x/x]$?