Converse of Deduction Theorem in Type Theory

Question

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!

Answer 1

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

According to the rules of simple type theory, we can then build the following derivation (a "converse" of the deduction theorem):

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