# If $\Gamma \vdash \phi$ then $\Gamma[v / c] \vdash \phi[v / c]$

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?

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]$$.

• could I ask why "case $v_1 = v$ is ruled out, as this would imply $v$ occurs in $\Gamma$"? Here is my understanding: $\Gamma$ is the premises/hypotheses of the deduction $D$, and if $v_1$ is not a free variable in any uncancelled hypotheses of deduction $D$, we can use $\forall I$ rule to get $\forall v_1 \phi(v_1)$. So I didn't think it was correct that $v_1 = v$ would imply that $v$ occurs in $\Gamma$; it might not occur at all, and using such $\forall I$ rule we could artificially bring it in. (though $v_1$ would not occur in $\phi(v_1)$ at all, as $v_1$ does not occur in $\phi$) – Albert Feb 24 at 4:28
• Maybe my understanding of expressions like $\phi(v_1)$ is mistaken? Am I only allowed to write that when $v_1$ appears as a free variable in $\phi$? (Or if $v_1$ does not appear in $\phi$, perhaps I am not allowed to write $\phi(v_1)$?) Please excuse my confusions, I am a beginner in Mathematical Logic. – Albert Feb 24 at 4:29
• No need for excuses, you were actually right and I was reading sloppily (I took $\Gamma$ to be the set of all formulas occuring in the proof). I have adapted the first paragraph, please let me know if it is clear now! – Timo Feb 24 at 11:32
• Concerning your second question about the meaning of the notation $\varphi(v_1)$: Unfortunately, this depends on the author. Sometimes it means that $v_1$ must occur freely in $\varphi$, sometimes it means that at most the variable $v_1$ appears freely in $\varphi$... You'll have to check in the lecture notes. – Timo Feb 24 at 11:44