3
$\begingroup$

I have a basic question about natural deduction and deduction theorem. I learn from my textbook that the deduction theorem

$$\textit{If }\ \Gamma,A\vdash B,\ \textit{ then }\ \Gamma\vdash A\rightarrow B.$$

corresponds to the introduction rule of $\rightarrow$ in natural deduction. This is trivially in fact. But what about the converse?

$$\textit{If }\ \Gamma\vdash A\rightarrow B,\ \textit{ then }\ \Gamma,A\vdash B.$$

It also holds. But what does it correspond to in natural deduction? Or how is it expressed in natural deduction?

It seems to me that the elimination rule of $\rightarrow$ does similar work, but it's different from the converse of the deduction theorem.

Thanks!

$\endgroup$
2
  • $\begingroup$ What book are you using? There are various different systems out there. $\endgroup$ – Noah Schweber Jul 29 '20 at 18:44
  • $\begingroup$ @NoahSchweber I am using van Dalen's Logic and Structure. $\endgroup$ – Kelly Jul 29 '20 at 18:49
7
$\begingroup$

Yes, it is just a quick consequence of the elimination rule.

$\to $ Elimination (in its most common phrasing) says that if $\Gamma\vdash A\to B$ and $\Gamma\vdash A$ then $\Gamma\vdash B.$

So, if $\Gamma\vdash A\to B,$ then $\Gamma, A\vdash A\to B.$ And of course $\Gamma,A\vdash A,$ so applying the elimination rule gives $\Gamma,A\vdash B.$

$\endgroup$
0

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.