In a previous post, I listed the rules of inference for quantifiers as they appear in a book I am studying (Chiswell & Hodges, Mathematical Logic). I don't particularly like the "reverse substitution" notation that they use to define the rules; I find it confusing and difficult to apply.
However, I have found an alternative set of rules that I find more to my liking (course notes found here) and want to confirm that these rules are correct and complete. More importantly, that my understanding of them is accurate, especially regarding restrictions. Here they are:
Definitions:
The notation $\phi[t/x]$ represents the formula $\phi$ after all free occurrences of the variable $x$ have been replaced with the term $t$, and $t$ is substitutable for $x$ in $\phi$
The term $t$ is substitutable for $x$ in $\phi$ only if no variables within $t$ become bound by any quantifier within $\phi$ as a result of replacing any free occurrences of $x$ with $t$
Universal elimination ($\forall E$)
If $\Gamma \vdash \forall x \phi$, then $\Gamma \vdash \phi[t/x]$
where $t$ is any term, $x$ is a variable, and $\phi$ is any formula. No restrictions apply.
Existential introduction ($\exists I$)
If $\Gamma \vdash \phi$, then $\Gamma \vdash \exists x \phi[x/t]$
where $t$ is a term, $\phi$ is a formula, and $x$ is a variable. No other restrictions apply.
Universal introduction ($\forall I$)
If $\Gamma \vdash \phi$, then $\Gamma \vdash \forall x \phi[x/v]$
where $v$ is a variable, $\phi$ is a formula, and $x$ is a variable. The variable $v$ must not appear free within any formula contained in $\Gamma$.
Existential elimination ($\exists E$)
If $\Gamma \vdash \exists x\phi$ and $\Gamma, \phi[v/x] \vdash \psi$, then $\Gamma \vdash \psi$
where $v$ is a variable, $\phi$ is a formula, and $x$ is a variable. The variable $v$ must not appear free within any formula contained in $\Gamma \cup \{\psi\}$.
I would like to know if there are any missing restrictions, any restrictions that are too broad, or anything incorrect or incomplete about these rules?