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!
-
$\begingroup$ The answer to this question tells you almost everything. $\endgroup$– TaroccoesbroccoJul 30, 2020 at 12:17
-
$\begingroup$ @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! $\endgroup$– ferdinandJul 30, 2020 at 12:49
-
$\begingroup$ @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? $\endgroup$– KellyJul 30, 2020 at 15:19
-
$\begingroup$ @Kelly - Not exactly, see my answer. $\endgroup$– TaroccoesbroccoJul 30, 2020 at 23:12
-
$\begingroup$ @Taroccoesbrocco Where is it? $\endgroup$– KellyJul 30, 2020 at 23:44
1 Answer
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.