3
$\begingroup$

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?

$\endgroup$
2
$\begingroup$

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

$\endgroup$
4
  • 1
    $\begingroup$ 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$) $\endgroup$ – Albert Feb 24 at 4:28
  • $\begingroup$ 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. $\endgroup$ – Albert Feb 24 at 4:29
  • 1
    $\begingroup$ 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! $\endgroup$ – Timo Feb 24 at 11:32
  • 1
    $\begingroup$ 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. $\endgroup$ – Timo Feb 24 at 11:44

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.