[proofplan]
We define two translations: one from natural deduction derivations to typed lambda terms, and one from typed lambda derivations to natural deduction derivations. Each translation is defined by induction on the final rule of the derivation. The three rules match exactly: assumption with variable, implication introduction with abstraction, and implication elimination with application. A final structural induction shows that the two translations are inverse to each other up to $\alpha$-renaming of bound variables.
[/proofplan]
[step:Fix the syntax and the labelled context convention]
Let $\mathsf{Var}$ be a [countable set](/page/Countable%20Set) of variables. A context $\Gamma$ is a finite partial function from $\mathsf{Var}$ to $\mathsf{Prop}_{\to}$; we write $x:A \in \Gamma$ to mean that $\Gamma$ assigns the formula $A$ to the variable $x$.
The simply typed lambda terms over $\mathsf{Var}$ are generated by the grammar
\begin{align*}
t ::= x \mid \lambda x:A.\,t \mid t\,u,
\end{align*}
where $x \in \mathsf{Var}$ and $A \in \mathsf{Prop}_{\to}$. The typing rules are:
\begin{align*}
&\frac{x:A \in \Gamma}{\Gamma \vdash x:A},
\\
&\frac{\Gamma, x:A \vdash t:B}{\Gamma \vdash \lambda x:A.\,t : A \to B},
\\
&\frac{\Gamma \vdash t:A \to B \qquad \Gamma \vdash u:A}{\Gamma \vdash t\,u:B}.
\end{align*}
The labelled natural deduction sequents use the same contexts. An open assumption labelled $x$ has formula $A$ exactly when $x:A \in \Gamma$. The rules are:
\begin{align*}
&\frac{x:A \in \Gamma}{\Gamma \vdash A},
\\
&\frac{\Gamma, x:A \vdash B}{\Gamma \vdash A \to B},
\\
&\frac{\Gamma \vdash A \to B \qquad \Gamma \vdash A}{\Gamma \vdash B}.
\end{align*}
In the implication introduction rule, the label $x$ records the discharged assumption. Bound labels are identified up to $\alpha$-renaming.
[/step]
[step:Translate each natural deduction derivation into a typed lambda term]
Define a translation $\Phi$ from labelled natural deduction derivations to typed lambda terms by induction on the last rule of the natural deduction derivation.
If the derivation is an assumption
\begin{align*}
\frac{x:A \in \Gamma}{\Gamma \vdash A},
\end{align*}
define $\Phi$ to be the variable $x$. The corresponding typing judgment is
\begin{align*}
\Gamma \vdash x:A.
\end{align*}
If the derivation ends by implication introduction
\begin{align*}
\frac{\Gamma, x:A \vdash B}{\Gamma \vdash A \to B},
\end{align*}
let $u$ be the term obtained by applying the induction hypothesis to the premise. Thus
\begin{align*}
\Gamma, x:A \vdash u:B.
\end{align*}
Define the translated term to be $\lambda x:A.\,u$. The abstraction typing rule gives
\begin{align*}
\Gamma \vdash \lambda x:A.\,u : A \to B.
\end{align*}
If the derivation ends by implication elimination
\begin{align*}
\frac{\Gamma \vdash A \to B \qquad \Gamma \vdash A}{\Gamma \vdash B},
\end{align*}
let $u$ and $v$ be the terms obtained from the two premises by the induction hypothesis. Then
\begin{align*}
\Gamma \vdash u:A \to B,
\qquad
\Gamma \vdash v:A.
\end{align*}
Define the translated term to be $u\,v$. The application typing rule gives
\begin{align*}
\Gamma \vdash u\,v:B.
\end{align*}
Therefore every labelled natural deduction derivation of $\Gamma \vdash A$ yields a typed lambda term $t$ with $\Gamma \vdash t:A$.
[guided]
We construct the lambda term by reading the proof from its final rule upward.
For an assumption, the proof says that the formula $A$ is available because the context contains a labelled assumption $x:A$. The matching lambda term is the variable $x$, and the variable typing rule gives
\begin{align*}
\Gamma \vdash x:A.
\end{align*}
For implication introduction, the natural deduction proof has the form
\begin{align*}
\frac{\Gamma, x:A \vdash B}{\Gamma \vdash A \to B}.
\end{align*}
The premise is a proof of $B$ under an additional assumption labelled $x$ of formula $A$. By the induction hypothesis, that premise already corresponds to a term $u$ with
\begin{align*}
\Gamma, x:A \vdash u:B.
\end{align*}
Discharging the assumption labelled $x$ is exactly the same operation as binding the variable $x$ in a lambda abstraction. Hence we assign to the whole derivation the term $\lambda x:A.\,u$, and the abstraction rule derives
\begin{align*}
\Gamma \vdash \lambda x:A.\,u : A \to B.
\end{align*}
For implication elimination, the natural deduction proof has premises
\begin{align*}
\Gamma \vdash A \to B,
\qquad
\Gamma \vdash A.
\end{align*}
By the induction hypothesis, these premises correspond to terms $u$ and $v$ satisfying
\begin{align*}
\Gamma \vdash u:A \to B,
\qquad
\Gamma \vdash v:A.
\end{align*}
Eliminating an implication means applying a proof of $A \to B$ to a proof of $A$; in lambda calculus this is application. Therefore the translated term is $u\,v$, and the application rule gives
\begin{align*}
\Gamma \vdash u\,v:B.
\end{align*}
These three cases exhaust the rules of implicational natural deduction, so the translation is defined for every derivation.
[/guided]
[/step]
[step:Translate each typed lambda derivation into a natural deduction derivation]
Define a translation $\Psi$ from typing derivations to labelled natural deduction derivations by induction on the last typing rule.
If the typing derivation is a variable rule
\begin{align*}
\frac{x:A \in \Gamma}{\Gamma \vdash x:A},
\end{align*}
define $\Psi$ to be the labelled assumption derivation
\begin{align*}
\frac{x:A \in \Gamma}{\Gamma \vdash A}.
\end{align*}
If the typing derivation ends by abstraction
\begin{align*}
\frac{\Gamma, x:A \vdash t:B}{\Gamma \vdash \lambda x:A.\,t : A \to B},
\end{align*}
apply the induction hypothesis to the premise to obtain a natural deduction derivation of
\begin{align*}
\Gamma, x:A \vdash B.
\end{align*}
Then apply implication introduction, discharging the assumption labelled $x$, to obtain
\begin{align*}
\Gamma \vdash A \to B.
\end{align*}
If the typing derivation ends by application
\begin{align*}
\frac{\Gamma \vdash t:A \to B \qquad \Gamma \vdash u:A}{\Gamma \vdash t\,u:B},
\end{align*}
apply the induction hypothesis to both premises to obtain natural deduction derivations of
\begin{align*}
\Gamma \vdash A \to B,
\qquad
\Gamma \vdash A.
\end{align*}
Then apply implication elimination to obtain
\begin{align*}
\Gamma \vdash B.
\end{align*}
Therefore every typing derivation $\Gamma \vdash t:A$ reconstructs a labelled natural deduction derivation of $\Gamma \vdash A$.
[guided]
We now reverse the previous construction. The last typing rule determines the last natural deduction rule.
If the typing derivation ends with a variable rule, then some $x:A$ belongs to $\Gamma$. A variable is the term-level form of an open assumption, so we reconstruct the natural deduction derivation
\begin{align*}
\frac{x:A \in \Gamma}{\Gamma \vdash A}.
\end{align*}
If the typing derivation ends with abstraction, then it has the form
\begin{align*}
\frac{\Gamma, x:A \vdash t:B}{\Gamma \vdash \lambda x:A.\,t : A \to B}.
\end{align*}
The induction hypothesis converts the premise into a natural deduction derivation of
\begin{align*}
\Gamma, x:A \vdash B.
\end{align*}
The variable $x$ is bound in the term $\lambda x:A.\,t$; on the proof side, this same binding operation is represented by discharging the assumption labelled $x$. Applying implication introduction gives
\begin{align*}
\Gamma \vdash A \to B.
\end{align*}
If the typing derivation ends with application, then it has premises
\begin{align*}
\Gamma \vdash t:A \to B,
\qquad
\Gamma \vdash u:A.
\end{align*}
The induction hypothesis converts these into natural deduction derivations of
\begin{align*}
\Gamma \vdash A \to B,
\qquad
\Gamma \vdash A.
\end{align*}
A proof of $A \to B$ together with a proof of $A$ gives a proof of $B$ by implication elimination. Thus we reconstruct a natural deduction derivation of
\begin{align*}
\Gamma \vdash B.
\end{align*}
These are precisely the three typing rules for the simply typed lambda calculus with function types, so every typing derivation is covered.
[/guided]
[/step]
[step:Verify that the two translations are inverse up to alpha-renaming]
We prove by induction on natural deduction derivations that applying $\Phi$ and then $\Psi$ returns the original natural deduction derivation up to $\alpha$-renaming of discharged assumption labels.
For an assumption derivation labelled $x$, the translation $\Phi$ gives the variable $x$, and $\Psi$ sends the variable rule back to the assumption labelled $x$.
For implication introduction, the derivation is obtained from a premise $\mathcal{D}$ of $\Gamma, x:A \vdash B$ by discharging $x$. By the induction hypothesis, $\Psi(\Phi(\mathcal{D}))$ is $\mathcal{D}$ up to $\alpha$-renaming. Applying implication introduction to both derivations gives the same conclusion $\Gamma \vdash A \to B$, with the same discharged label after possibly renaming the bound label $x$.
For implication elimination, the derivation is obtained from premises $\mathcal{D}_1$ of $\Gamma \vdash A \to B$ and $\mathcal{D}_2$ of $\Gamma \vdash A$. By the induction hypothesis, each premise is recovered up to $\alpha$-renaming. Applying implication elimination to the recovered premises gives the original conclusion $\Gamma \vdash B$.
The same induction on typing derivations proves that applying $\Psi$ and then $\Phi$ returns the original typed lambda derivation up to $\alpha$-renaming of bound variables. The variable case returns the same variable. The abstraction case uses the induction hypothesis on the body derivation and then rebuilds the abstraction $\lambda x:A.\,t$, allowing renaming of the bound variable $x$. The application case uses the induction hypothesis on both subderivations and then rebuilds the application $t\,u$.
Thus $\Phi$ and $\Psi$ are mutually inverse up to $\alpha$-renaming. Hence labelled natural deduction derivations of $\Gamma \vdash A$ in implicational intuitionistic logic correspond bijectively to typed lambda terms $t$ satisfying $\Gamma \vdash t:A$, with assumptions, implication introduction, and implication elimination matching variables, abstraction, and application respectively.
[/step]
