4
$\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$ Commented Jul 29, 2020 at 18:44
  • $\begingroup$ @NoahSchweber I am using van Dalen's Logic and Structure. $\endgroup$
    – Kelly
    Commented Jul 29, 2020 at 18:49

1 Answer 1

10
$\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

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .