# Converse of Deduction Theorem

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!

• What book are you using? There are various different systems out there. Jul 29, 2020 at 18:44
• @NoahSchweber I am using van Dalen's Logic and Structure. Jul 29, 2020 at 18:49

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