Is the following set of inference rules for quantifiers in ND correct?

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?

• Nitpicking comment regarding the "usual" convention about meta-variables (from van Dalen, page 63): "we will write down (meta-) expressions like $ϕ(x, y, z),ψ(x,x)$, etc. This neither means that the listed variables occur free nor that no other ones occur free. It is merely a convenient way to handle substitution informally: $ϕ(t)$ is the result of replacing $x$ by $t$ in $ϕ(x)$." – Mauro ALLEGRANZA Jan 10 '18 at 14:17
• The above to point at an excess of restriction in e.g. $\forall$I: "$ϕ$ is a formula containing $v$". The substitution $\bot [t/x] := \bot$ is syntactically correct and allowed. In the same way, the "null" quantification: $\forall x (0=0)$ is syntactically correct. Thus means that the derivation $0=0 \vdash \forall x (0=0)$ is a legitimate application of $\forall$I. – Mauro ALLEGRANZA Jan 10 '18 at 14:20
• Ok, I have changed this to "$\phi$ is a formula". – esotechnica Jan 10 '18 at 14:27
• Is there an excess of restriction in the same manner for $\exists I$? That is, should I change this to "$\phi$ is a formula" within $\exists I$, rather than "$\phi$ is a formula containing t" – esotechnica Jan 10 '18 at 14:30
• If you agree that $\phi [x/t]$ is defined also when $t$ is not occurring in $\phi$, then yes: there is no restriction needed on $\phi$. – Mauro ALLEGRANZA Jan 10 '18 at 14:38

As pointed out in the comments, it is unusual to think of the quantifier rules in terms of substituting variables for terms. It's not you can't, but if you do, your rules can become unnecessarily restrictive, as you yourself also pointed out. That is, if we say that $\phi[x/t]$ is the formula that one obtains by replacing all instances of $t$ with $x$, then the $\exists \ I$ rule cannot go from something like $A(b,b)$ to $\exists x \ A(b,x)$, even though that is of course a perfectly valid inference.

So, it's better to define something like $\exists \ I$ as:

If $\phi[t/x]$, then $\exists x \ \phi$

And yes, that feels a bit backward, in that the substitution seems to go from conclusion to premise, but think of it as a 'check' on whether the rule has been applied correctly or not: Whenever someone tries to infer $\exists x \ \phi(x)$ from some formula $\phi$, is it true that there is some term $t$ such that if we replace all free occurrences of $x$ in $\phi(x)$ with $t$, we end up with the original $\phi$?

And yes, maybe that's all a bit more intuitive if you write the rule simply as:

If $\phi(t)$, then $\exists x \ \phi(x)$

But also think about this: There may not be any $t$'s being replaced with variables at all. That is, you can go from $A(b,b)$ to $\exists x \ A(b,b)$. Why? Because in accordance to the rule as I defined it above, we can pick any term $t$, replace all free variables in the $A(b,b)$ that comes after the $\exists \ x$ in $\exists x \ A(b,b)$ with that $t$, and the result is indeed $A(b,b)$. So, in that sense, seeing the substitution process as going 'from' $\phi(t)$ 'to' $\phi(x)$ again makes less sense than if you think of it as going 'from' $\phi(x)$ 'to' $\phi(t)$