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).