I'm taking a course in Mathematical Logic, and in the lectures there was the proposition:
Suppose $\Gamma \vdash \phi$ and $v$ is a variable that is not occurring in $\Gamma$ or $\phi .$ If $\Gamma \vdash \phi$ then $\Gamma[v / c] \vdash \phi[v / c]$ where $\Gamma[v / c]:=\{\theta[v / c]: \theta \in \Gamma\}$.
Here, I think $\Gamma$ is a set of $\mathcal{L}$-formulas, $\phi$ is an $\mathcal{L}$-formula, $v$ is an $\mathcal{L}$-variable, and $c$ is an $\mathcal{L}$-constant. The proof of this is left as an exercise, the hint being to use induction on length of proof. I have done the induction steps for the rules $\forall I$, $\to I$, $\to E$, $\land I$, $\land E$, $\bot$, and $RAA$. However, I am struggling to do the $\forall E$ rule.
For example, suppose we have a deduction $D \cdots \forall v_1 \phi(v_1) \vdash \phi(t)$, where $t$ is free for $v_1$ in $\phi(v_1)$. By the induction hypothesis, we then have $D[v/c] \cdots \vdash \forall v_1 \phi(v_1) [v/c]$, and from this we must deduce $D[v/c] \cdots (\forall v_1 \phi(v_1))[v/c] \vdash \phi(t)[v/c]$. By assumption, $v$ does not occur in $\phi(t)$.
If $v_1 \neq v$, then $v$ is free for $c$ in $\phi(v_1)$, because $v$ does not even occur in $\phi(v_1)$ (as $v$ does not occur in $\phi(t)$). Thus, $\forall v_1 \phi(v_1) [v/c]$ is $\forall v_1 (\phi[v/c])(v_1)$ as variable capture does not happen. As $t$ is still free for $v_1$ in $\phi[v/c]$, we use $\forall E$ rule to deduce $D \cdots \forall v_1 (\phi[v/c])(v_1) \vdash (\phi[v/c])(t)$. Now I should somehow conclude that $(\phi[v/c])(t)$ is equal to $(\phi(t))[v/c]$, but I don't know how to do this.
Furthermore, if $v_1 = v$, then I am totally lost about what to do. I tried to argue that the deduction $D \cdots \forall v_1 \phi(v_1) \vdash \phi(t)$ somehow implied that $v_1$ appeared in a hypothesis of $D$, thus $v_1$ appears in $\Gamma$, but I don't know if this is even a correct argument, much less make it rigorous.
Could anyone help me with this? Maybe I'm doing something wrong?
Best Answer
Assume your proof ends with $D \cdots \forall v_1 \phi(v_1) \vdash \phi(t)$.
[EDIT: The following paragraph is a correction following a comment from Albert.]
If $v_1=v$, first rename all bound occurences of $v_1$ in the derivation $D \cdots \forall v_1 \phi(v_1)$ to a variable $v_1'\neq v$ which does not yet occur in the proof. All rules remain sound, and $D$ is not affected since it contains no occurences of $v$ (bound or free) by assumption. In this way you obtain a derivation $D \cdots \forall v_1' \phi(v_1')$ where $v_1'\neq v$.
Hence we can now assume $v_1\neq v$. By induction hypothesis we get a proof ending with $\forall v_1 (\varphi[v/c])(v_1)$. As you noted, what we ultimately want to get is a proof of $\varphi(t)[v/c]$. The trick is to apply $\forall E$ instantiating $v_1$ with $t[v/c]$ (instead of $t$). In this way you obtain the formula $\varphi[v/c](t[v/c])$, and this is indeed identical to $\varphi(t)[v/c]$.
The intuition is that $t$ might contain occurences of $c$, and so if you first replace all $c$'s by $v$'s and then all $v_1$'s by $t$'s, then the latter step reintroduces some $c$'s into your formula that you don't want to have. Consider for example the case that $\varphi=P(v_1)$, $t=c$ and your initial proof is $\forall v_1 P(v_1)\vdash P(c)$. The proposition says that you should be able to obtain a proof of $\forall v_1 P(v_1)\vdash P(v)$. Clearly you should not instantiate $v_1$ with $t=c$, but rather with $v=t[v/c]$.