First order logic natural deduction problem

Question

I am struggling with a particular case in the (inductive) proof of Theorem 2.8.3 (i) of Logic and Structure by Dirk Van Dalen ($c \neq x$ in the Theorem statement is a variable)

The cases when we consider proof trees for $\Gamma \vdash \phi$ for all rules but and-elimination/if-elimination I don't encounter any difficulty with as the inductive hypothesis (on the weight of proof tree) can be straightforwardly applied, but when the proof tree is that of and-elimination (say), the parent of the consequent may have occurrences of the variable $x$. To make matters worse I couldn't eliminate the problem by attempting to use the induction hypothesis with a 'fresh' variable $m$ replacing all occurrences of $x$ in the parent of the consequent since all such occurrences may be bound.

Any help with this matter would be much appreciated.

Answer 1

A priori, you are right, there might be a problem in the rules $\land_E$ and $\to_E$, because the . But in fact, the problem is easily solved because there is another nice property for natural deduction:

Lemma: If $\Gamma \vdash \varphi$ and $x \in FV(\varphi)$ then $x \in FV(\psi)$ for some $\psi \in \Gamma$.

This lemma can be easily proved by induction on the derivation of $\Gamma \vdash \varphi$ (if you prefer, you can prove it simultaneously to the proof of van Dalen's Theorem 2.8.3.(i)). Note that you are in language where the only connectives are $\land, \to, ⊥$ and $\forall$ (p. 91).

Thanks to the lemma above, you do not have any problem in the proof of Theorem 2.8.3.(i) with the cases $\land_E$ and $\to_E$. For instance, for $\land_{E_i}$ (with $i \in \{1,2\}$), you have that \begin{align} \dfrac{\quad\Gamma\\\quad \ \vdots\\\varphi_1 \land \varphi_2}{\varphi_i}\land_{E_i} \end{align} According to your hypothesis, $x$ does not occur in $\Gamma$ or $\varphi_i$, but what about $\varphi_j$ with $j\neq i$? By the lemma above, if $x$ occurred free in $\varphi_j$ then $x$ would occur free in $\Gamma$, which contradicts the hypothesis. So, $x \notin FV(\varphi_j)$. Moreover, if $x$ occurred bound in $\varphi_j$ then you could rename bound variables in $\varphi_j$ so that $x$ does not occur bound in $\varphi_j$. Therefore, $x$ do not occur in $\Gamma$ or $\varphi_1$ or $\varphi_2$. Hence, you can apply the inductive hypothesis to the derivation of $\Gamma \vdash \varphi \land \varphi_2$. Then, you can easily conclude by yourself.