# First order logic natural deduction problem

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.

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.

• Thank you kindly for your reply, if I am understanding correctly, this helper lemma eliminates some difficulty but if $\phi_j = \phi_2 \neq \phi_1$ contains bound occurrences of $x$, would we not need another helper lemma giving us a proof of $\phi_1 \wedge \phi_2^{*}$ where $\phi_2^{*}$ is $\phi_2$ with all bound occurrences of $x$ replaced by a new variable, of the same weight as the and elimination tree $\wedge_{E_i}$ in your answer, so that we can proceed and apply the inductive hypothesis? – porridgemathematics Jun 4 '20 at 11:32
• Basically its the '" rename all bound variables in $\phi_j$ " that is troubling me. – porridgemathematics Jun 4 '20 at 11:41
• Also isn't the lemma false as stated? Consider $\{ \forall x. (x=x)\} \vdash (v=v)$ where $v \neq x$, clearly $v$ is free in the consequent, but not free in any hypothesis? – porridgemathematics Jun 4 '20 at 11:46
• (answer to the first two comments) - Yes, but actually this further lemma is implicit, because formulas in predicate logic can be identified up to renaming of bound variables. In other words, for instance, $\forall x \, x = x$ and $\forall y \, y =y$ are the same formula. See Theorem 2.5.6 in van Dalen's textbook. – Taroccoesbrocco Jun 4 '20 at 11:50
• Oh I see! I overlooked this completely as I hadn't looked over that theorem (I am actually using notes that are only loosely based on Van Dalen's text), will do now – porridgemathematics Jun 4 '20 at 11:54