# Inference rules for quantifiers in natural deduction - are all the conditions correct?

Because I am getting quite confused with the definition of the four inference rules for quantifiers, and all of their conditions, I would like to write them down here as I understand it. My questions follow afterwards:

Preliminaries

The substitution $\phi[t/x]$ represents the formula $\phi$ after all free variables $x$ are replaced in $\phi$ with the term $t$. The term $t$ can be a constant, variable or function expression, but $x$ must be a variable

The term $t$ is said to be substitutable if when performing the substitution $\phi[t/x]$, no variables within $t$ become bound by any quantifier within $\phi$.

Universal elimination

If $\Gamma \vdash \forall x\, \phi$, then $\Gamma \vdash \phi[t/x]$.

Restrictions:

• $t$ can be any term (constant, variable or function expression) that must be substitutable for $x$ within $\phi$.

Existential introduction

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

Restrictions:

• $t$ can be any term (constant, variable or function expression) that must be substitutable for $x$ within $\phi$.

Universal introduction

If $\Gamma \vdash \phi[t/x]$, then $\Gamma \vdash \forall x \, \phi$.

Restrictions:

• $t$ can be any term (constant, variable or function expression) that must be substitutable for $x$ within $\phi$

• $t$ cannot be present in any formula within $\Gamma$.

Existential elimination

If $\Gamma \vdash \exists x \,\phi$ and $\Gamma, \phi[t/x] \vdash \psi$, then $\Gamma \vdash \psi$.

Restrictions:

• $t$ can be any term (constant, variable or function expression) that must be substitutable for $x$ within $\phi$

• $t$ can not be present in $\phi$

• $t$ cannot be present in $\psi$

• $t$ cannot be present in any formulas within $\Gamma$.

My questions then, are:

• Are these rules correct and complete? Are any restrictions missing, unnecessary, or are there any restrictions that are too restrictive?

• I'm particularly suspect about the conditions on $\forall I$ and $\exists E$, which state that "$t$ cannot be present in any formulas within $\Gamma~$". I feel like this can be relaxed to "$t$ cannot be free in any formulas within $\Gamma~$". Or am I wrong? For instance, shouldn't you be able to derive the following sequent: $\forall x \, Px \vdash \forall x(x = 0 \vee \forall x \, Px)$, which would not be possible with the restrictions as they stand.

$\def\fitch#1#2{\begin{array}{|l}#1 \\ \hline #2\end{array}}$ $$\fitch { 1. \qquad \forall x Px \qquad (A) }{ 2. \qquad x = 0 \vee \forall x Px \qquad (\vee I) \\ 3. \qquad \forall x(x = 0 \vee \forall x Px) \qquad (\forall I: ) }$$

• The definition for substitution in Chiswell and Hodges Mathematical Logic seems to require that a term $t$ be substitutable for any substitution (Definition 7.27 pg. 167). That is, $t$ being substitutable is implied in any substitution. Therefore, I think I could embed the concept of substitutability within the definition of substitution itself, and can remove the first restriction from each of these inference rules. However, others have said that the two concepts are independent. That is, a substitution can occur without a term being substitutable. This seems strange to me; indeed Chiswell and Hodges say that such a substitution is "meaningless"(p. 183) and "undefined" (p. 167).
• Correct: in ∀I the variable $x$ may not occur free in any hypothesis on which $ϕ(x)$ depends. – Mauro ALLEGRANZA Jan 9 '18 at 14:28
• As you can see from page 110, C&H follows a "reverse" approach: they first define sustitutable for (or free for) in Def.5.2.9 and then they define the opertion of substitution in term of the previous one (Def.5.2.10). In this way, substitutions are preformed only if the "substitutability" condition holds. – Mauro ALLEGRANZA Jan 9 '18 at 14:34
• You must take into account that C&H use a term $t$ in the statement of the rule. $t$ can be a variable $y$, a constant $c$ or a "complex" term like $f(x)$ of $f(c)$. Only variables may be quantified and we do not quantify constants and "complex" terms. Thus, tehy cannot write: "$t$ free". – Mauro ALLEGRANZA Jan 9 '18 at 14:41
• Correct; your derivation above is sound. So, if the rule is expressed only withrespect to variables, the restriction is: "$x$ does not occur free". If the rule is expressed for terms, you have to manage the different cases. – Mauro ALLEGRANZA Jan 9 '18 at 16:05
• I do not agree; the derivation can be simply written as follows: $\forall x Px \vdash y=0 \lor \forall x Px \vdash \forall x (x=0 \lor \forall x Px)$. – Mauro ALLEGRANZA Jan 9 '18 at 16:42