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)

Theorem 2.8.3

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.

  • $\begingroup$ 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? $\endgroup$ – porridgemathematics Jun 4 '20 at 11:32
  • $\begingroup$ Basically its the '" rename all bound variables in $\phi_j$ " that is troubling me. $\endgroup$ – porridgemathematics Jun 4 '20 at 11:41
  • $\begingroup$ 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? $\endgroup$ – porridgemathematics Jun 4 '20 at 11:46
  • $\begingroup$ (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. $\endgroup$ – Taroccoesbrocco Jun 4 '20 at 11:50
  • $\begingroup$ 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 $\endgroup$ – porridgemathematics Jun 4 '20 at 11:54

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.