# Converse of Deduction Theorem in Type Theory

I have a question about the way to express the converse of the deduction theorem in type theory. In simple type theory, the deduction theorem can be easily expressed by the introduction rule for $$\rightarrow$$, namely: $$\frac{\Gamma, x:A\vdash b(x):B}{\Gamma\vdash(\lambda x)b(x):A\rightarrow B.}$$ The converse of the deduction theorem also holds, from a logical point of view. But I wonder how it is expressed in type theory. Thanks a lot!

• The answer to this question tells you almost everything. Jul 30, 2020 at 12:17
• @Taroccoesbrocco Thanks! It's almost everything! But I wonder how to express $\frac{\Gamma, A\vdash A,\quad\Gamma, A\vdash A\rightarrow B}{\Gamma, A\vdash B}$ in type theory. It does not look like typed $\rightarrow$-elimination. How can I write this in type theory? Thanks! Jul 30, 2020 at 12:49
• @Taroccoesbrocco@ferdinand Perhaps: $\frac{\Gamma, x:A\vdash x:A,\quad\Gamma, x:A\vdash(\lambda x)b(x):A\rightarrow B}{\Gamma, x:A\vdash b(x):B}$. This is a literal typed translation. I also find it strange because it seems that I am using $x:A$ as a substitution. Is that right? Jul 30, 2020 at 15:19
• @Kelly - Not exactly, see my answer. Jul 30, 2020 at 23:12
• @Taroccoesbrocco Where is it? Jul 30, 2020 at 23:44

In type theory, the converse of deduction theorem holds from a logical point of view: as explained here, if $$\Gamma \vdash A \to B$$ is derivable then $$\Gamma, A \vdash B$$ is derivable. But the $$\lambda$$-term associated with the derivation of $$\Gamma, A \vdash B$$ in the converse of the deduction theorem is not the $$\lambda$$-term associated with the derivation of $$\Gamma, A \vdash B$$ in the deduction theorem.
Indeed, suppose that $$\Gamma \vdash A \to B$$ is derivable. We can suppose without loss of generality that $$A \notin \Gamma$$, because it is immediate to prove that if $$\Gamma \vdash A \to B$$ is derivable then $$\Gamma, A \vdash A \to B$$ (I assume the logical rules of the deductive system are the ones listed here). Now, consider a derivation of $$\Gamma, A \vdash A \to B$$. Which is the $$\lambda$$-term associated with such a derivation? When decorated with $$\lambda$$-terms, the conclusion of the derivation is something of the form $$\Gamma, x : A \vdash t : A \to B$$. Note that $$t$$ need not be of the form $$\lambda x.b$$: for instance, $$t$$ could be a variable, provided that $$A \to B \in \Gamma$$.
$$\dfrac{\qquad \vdots \\ \Gamma, x : A \vdash t : A \to B \qquad \dfrac{}{\Gamma, x : A \vdash x : A}{\scriptstyle\text{ax}}}{\Gamma, x : A \vdash tx : B}\to_\text{elim}$$
Not that the $$\lambda$$-term $$tx$$ is different from the $$\lambda$$-term $$b$$ that decorates the derivation of $$\Gamma, A \vdash B$$ in the deduction theorem.