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!
Best Answer
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.$