[proofplan] We make the proposition-to-type translation explicit and then prove the correspondence by induction on derivations in both directions. In the natural-deduction-to-typing direction, each introduction rule becomes the corresponding constructor and each elimination rule becomes the corresponding eliminator. In the typing-to-natural-deduction direction, the same table is read backwards. Finally, the beta and eta equalities are checked rule by rule, because each beta law removes an introduction immediately followed by its matching elimination, while each eta law expands an arbitrary proof into its canonical elimination-introduction form. [/proofplan]

[step:Define the translation on propositions and contexts] Let $\mathsf{At}$ denote the set of atomic propositions, and let $\mathsf{At}^\ast$ denote the corresponding set of atomic simple types. Define the map \begin{align*} (-)^\ast:\mathsf{Prop}_{\mathsf{IPC}}\to\mathsf{Ty}_{\lambda} \end{align*} by recursion on propositions. For an atomic proposition $P\in\mathsf{At}$, the type $P^\ast\in\mathsf{At}^\ast$ is the corresponding atomic type. For compound propositions the clauses are \begin{align*} (P\to Q)^\ast = P^\ast\to Q^\ast. \end{align*} \begin{align*} (P\wedge Q)^\ast = P^\ast\times Q^\ast. \end{align*} \begin{align*} (P\vee Q)^\ast = P^\ast+Q^\ast. \end{align*} \begin{align*} \top^\ast=\mathbf{1}. \end{align*} \begin{align*} \bot^\ast=\mathbf{0}. \end{align*} If $\Gamma=P_1,\dots,P_n$ is a list of assumption occurrences, define its translated typing context by \begin{align*} \Gamma^\ast=x_1:P_1^\ast,\dots,x_n:P_n^\ast, \end{align*} where $x_1,\dots,x_n$ are pairwise distinct variables. Repeated occurrences of the same proposition are treated as distinct assumptions and therefore receive distinct variables. Structural rules on natural deduction contexts correspond to weakening, exchange, and contraction for variables in typing contexts. We use the following typed constructors and eliminators. For product types, $\pi_1$ and $\pi_2$ denote the first and second projections. For sum types, $\operatorname{inl}$ and $\operatorname{inr}$ denote the left and right injections, and $\operatorname{case}(s;x.u;y.v)$ denotes the sum eliminator with scrutinee $s$ and branches binding variables $x$ and $y$. The symbol $\ttstar$ denotes the unique constructor of the unit type $\mathbf{1}$, $\operatorname{let}_{\mathbf{1}}(r;c)$ denotes the unit eliminator with unit-typed scrutinee $r$ and branch term $c$, and $\operatorname{abort}_{A}(e)$ denotes the empty type eliminator from $e:\mathbf{0}$ into the type $A$. [/step]

[step:Translate natural deduction derivations into typed lambda terms]We prove, by induction on a natural deduction derivation $\mathcal{D}$ of $\Gamma\vdash Q$, that there is a term $t$ with \begin{align*} \Gamma^\ast\vdash t:Q^\ast. \end{align*} If $\mathcal{D}$ is the assumption rule selecting the $i$th assumption $P_i$ in $\Gamma$, take $t=x_i$. Then $x_i:P_i^\ast$ occurs in $\Gamma^\ast$, so the variable typing rule gives \begin{align*} \Gamma^\ast\vdash x_i:P_i^\ast. \end{align*} For implication introduction, suppose the last rule derives $\Gamma\vdash P\to Q$ from a derivation of $\Gamma,P\vdash Q$. By the induction hypothesis, for a fresh variable $x:P^\ast$ there is a term $u$ such that \begin{align*} \Gamma^\ast,x:P^\ast\vdash u:Q^\ast. \end{align*} The function introduction rule gives \begin{align*} \Gamma^\ast\vdash \lambda x.u:P^\ast\to Q^\ast. \end{align*} Since $(P\to Q)^\ast=P^\ast\to Q^\ast$, this is the required typing judgment. For implication elimination, suppose the last rule derives $\Gamma\vdash Q$ from derivations of $\Gamma\vdash P\to Q$ and $\Gamma\vdash P$. By the induction hypothesis there are terms $f$ and $a$ such that \begin{align*} \Gamma^\ast\vdash f:P^\ast\to Q^\ast. \end{align*} \begin{align*} \Gamma^\ast\vdash a:P^\ast. \end{align*} The application rule gives \begin{align*} \Gamma^\ast\vdash f(a):Q^\ast. \end{align*} For conjunction introduction, derivations of $\Gamma\vdash P$ and $\Gamma\vdash Q$ translate to terms $a:P^\ast$ and $b:Q^\ast$ in context $\Gamma^\ast$. The product introduction rule gives \begin{align*} \Gamma^\ast\vdash (a,b):P^\ast\times Q^\ast. \end{align*} For conjunction elimination, a derivation of $\Gamma\vdash P\wedge Q$ translates to $p:P^\ast\times Q^\ast$, and the product projection rules give \begin{align*} \Gamma^\ast\vdash \pi_1(p):P^\ast. \end{align*} \begin{align*} \Gamma^\ast\vdash \pi_2(p):Q^\ast. \end{align*} For disjunction introduction, a derivation of $\Gamma\vdash P$ translates to $a:P^\ast$, and the left sum injection gives \begin{align*} \Gamma^\ast\vdash \operatorname{inl}(a):P^\ast+Q^\ast. \end{align*} A derivation of $\Gamma\vdash Q$ translates to $b:Q^\ast$, and the right sum injection gives \begin{align*} \Gamma^\ast\vdash \operatorname{inr}(b):P^\ast+Q^\ast. \end{align*} For [disjunction elimination](/theorems/4625), suppose the last rule has premises $\Gamma\vdash P\vee Q$, $\Gamma,P\vdash R$, and $\Gamma,Q\vdash R$. The induction hypothesis gives terms \begin{align*} \Gamma^\ast\vdash s:P^\ast+Q^\ast. \end{align*} \begin{align*} \Gamma^\ast,x:P^\ast\vdash u:R^\ast. \end{align*} \begin{align*} \Gamma^\ast,y:Q^\ast\vdash v:R^\ast. \end{align*} The sum eliminator gives \begin{align*} \Gamma^\ast\vdash \operatorname{case}(s;x.u;y.v):R^\ast. \end{align*} For truth introduction, the unique natural deduction proof of $\top$ translates to the unit term: \begin{align*} \Gamma^\ast\vdash \ttstar:\mathbf{1}. \end{align*} For truth elimination, suppose the last rule derives $\Gamma\vdash R$ from derivations of $\Gamma\vdash\top$ and $\Gamma\vdash R$. The induction hypothesis gives terms $r$ and $c$ such that \begin{align*} \Gamma^\ast\vdash r:\mathbf{1}. \end{align*} \begin{align*} \Gamma^\ast\vdash c:R^\ast. \end{align*} The unit eliminator gives \begin{align*} \Gamma^\ast\vdash \operatorname{let}_{\mathbf{1}}(r;c):R^\ast. \end{align*} For falsehood elimination, a derivation of $\Gamma\vdash\bot$ translates to a term $e:\mathbf{0}$, and the empty type eliminator gives, for every proposition $Q$, \begin{align*} \Gamma^\ast\vdash \operatorname{abort}_{Q^\ast}(e):Q^\ast. \end{align*} These cases exhaust the natural deduction rules for implication, conjunction, disjunction, truth, and falsehood, so the induction proves the first direction.[/step]

[guided]We want to prove that every proof becomes a typed term. The right method is induction on the final rule of the natural deduction derivation, because natural deduction derivations are built by repeatedly applying introduction and elimination rules. First consider the assumption rule. If the derivation ends by using the $i$th assumption $P_i$ from the context \begin{align*} \Gamma=P_1,\dots,P_n, \end{align*} then the translated context is \begin{align*} \Gamma^\ast=x_1:P_1^\ast,\dots,x_n:P_n^\ast. \end{align*} The variable $x_i$ has type $P_i^\ast$ in this context, so the translated proof term is $x_i$ and the typing judgment is \begin{align*} \Gamma^\ast\vdash x_i:P_i^\ast. \end{align*} For implication introduction, the natural deduction rule says that a derivation of $Q$ from the extra assumption $P$ gives a derivation of $P\to Q$. Translating the premise by the induction hypothesis gives a term $u$ in the extended typing context: \begin{align*} \Gamma^\ast,x:P^\ast\vdash u:Q^\ast. \end{align*} The corresponding typed lambda operation is abstraction. Therefore \begin{align*} \Gamma^\ast\vdash \lambda x.u:P^\ast\to Q^\ast. \end{align*} Since the translation sends implication to function type, this is exactly a term of type $(P\to Q)^\ast$. For implication elimination, the natural deduction rule is modus ponens: from proofs of $P\to Q$ and $P$, obtain a proof of $Q$. By induction, the two premises translate to \begin{align*} \Gamma^\ast\vdash f:P^\ast\to Q^\ast. \end{align*} \begin{align*} \Gamma^\ast\vdash a:P^\ast. \end{align*} The typed lambda calculus eliminator for function type is application, so the translated conclusion is \begin{align*} \Gamma^\ast\vdash f(a):Q^\ast. \end{align*} For conjunction, the introduction rule combines proofs of $P$ and $Q$. The induction hypothesis gives terms \begin{align*} \Gamma^\ast\vdash a:P^\ast. \end{align*} \begin{align*} \Gamma^\ast\vdash b:Q^\ast. \end{align*} The product constructor forms the pair: \begin{align*} \Gamma^\ast\vdash (a,b):P^\ast\times Q^\ast. \end{align*} Because $(P\wedge Q)^\ast=P^\ast\times Q^\ast$, this is the translation of conjunction introduction. The two conjunction eliminations are projections. If \begin{align*} \Gamma^\ast\vdash p:P^\ast\times Q^\ast, \end{align*} then the product elimination rules give \begin{align*} \Gamma^\ast\vdash \pi_1(p):P^\ast. \end{align*} \begin{align*} \Gamma^\ast\vdash \pi_2(p):Q^\ast. \end{align*} For disjunction, the left introduction rule sends a proof of $P$ to a proof of $P\vee Q$. If the premise translates to \begin{align*} \Gamma^\ast\vdash a:P^\ast, \end{align*} then the translated term is the left injection: \begin{align*} \Gamma^\ast\vdash \operatorname{inl}(a):P^\ast+Q^\ast. \end{align*} The right introduction rule is analogous: from \begin{align*} \Gamma^\ast\vdash b:Q^\ast \end{align*} we get \begin{align*} \Gamma^\ast\vdash \operatorname{inr}(b):P^\ast+Q^\ast. \end{align*} The elimination rule for disjunction is case analysis. A natural deduction proof of $R$ from $P\vee Q$ uses a proof of the disjunction, a derivation of $R$ assuming $P$, and a derivation of $R$ assuming $Q$. The induction hypothesis translates these three pieces as \begin{align*} \Gamma^\ast\vdash s:P^\ast+Q^\ast. \end{align*} \begin{align*} \Gamma^\ast,x:P^\ast\vdash u:R^\ast. \end{align*} \begin{align*} \Gamma^\ast,y:Q^\ast\vdash v:R^\ast. \end{align*} The sum eliminator combines them: \begin{align*} \Gamma^\ast\vdash \operatorname{case}(s;x.u;y.v):R^\ast. \end{align*} For truth, the proposition $\top$ translates to the unit type $\mathbf{1}$. The truth introduction rule has no premises, and the corresponding term constructor is the unique unit term: \begin{align*} \Gamma^\ast\vdash \ttstar:\mathbf{1}. \end{align*} The truth eliminator is translated by the unit eliminator. If the induction hypothesis gives \begin{align*} \Gamma^\ast\vdash r:\mathbf{1} \end{align*} and \begin{align*} \Gamma^\ast\vdash c:R^\ast, \end{align*} then the unit eliminator gives \begin{align*} \Gamma^\ast\vdash \operatorname{let}_{\mathbf{1}}(r;c):R^\ast. \end{align*} For falsehood, the proposition $\bot$ translates to the empty type $\mathbf{0}$. The elimination rule for falsehood says that anything follows from a contradiction. If the induction hypothesis gives \begin{align*} \Gamma^\ast\vdash e:\mathbf{0}, \end{align*} then the empty type eliminator gives, for every proposition $Q$, \begin{align*} \Gamma^\ast\vdash \operatorname{abort}_{Q^\ast}(e):Q^\ast. \end{align*} Every rule of the stated natural deduction fragment appears in one of these cases. Therefore induction on derivations gives, for each derivation of $\Gamma\vdash Q$, a typed lambda term $t$ satisfying \begin{align*} \Gamma^\ast\vdash t:Q^\ast. \end{align*}[/guided]

[step:Translate typing derivations back into natural deduction derivations]We prove the converse by induction on a typing derivation of \begin{align*} \Gamma^\ast\vdash t:Q^\ast. \end{align*} Because the simply typed lambda calculus in the statement has atomic types only from $\mathsf{At}^\ast$, every type appearing in a derivation of $\Gamma^\ast\vdash t:Q^\ast$ is generated from $\mathsf{At}^\ast$ by $\to$, $\times$, $+$, $\mathbf{1}$, and $\mathbf{0}$. Hence every such type lies in the image of $(-)^\ast$ and corresponds uniquely to a proposition generated by $\to$, $\wedge$, $\vee$, $\top$, and $\bot$. If the last rule is the variable rule for $x_i:P_i^\ast$, the corresponding natural deduction derivation is the assumption rule for $P_i$ in $\Gamma$. If the last rule is function introduction, then $t=\lambda x.u$ and the premise has the form \begin{align*} \Gamma^\ast,x:P^\ast\vdash u:Q^\ast. \end{align*} By induction this gives a natural deduction derivation of $\Gamma,P\vdash Q$. Implication introduction gives $\Gamma\vdash P\to Q$. If the last rule is function elimination, then $t=f(a)$ with premises \begin{align*} \Gamma^\ast\vdash f:P^\ast\to Q^\ast \end{align*} and \begin{align*} \Gamma^\ast\vdash a:P^\ast. \end{align*} By induction these give derivations of $\Gamma\vdash P\to Q$ and $\Gamma\vdash P$. Implication elimination gives $\Gamma\vdash Q$. Product introduction translates back to conjunction introduction, and the two product projections translate back to the two conjunction elimination rules. Sum injections translate back to the two disjunction introduction rules, and the sum case eliminator translates back to disjunction elimination. The unit introduction rule translates back to truth introduction. If the last rule is unit elimination, then $t=\operatorname{let}_{\mathbf{1}}(r;c)$ with premises \begin{align*} \Gamma^\ast\vdash r:\mathbf{1} \end{align*} and \begin{align*} \Gamma^\ast\vdash c:R^\ast. \end{align*} By induction these give natural deduction derivations of $\Gamma\vdash\top$ and $\Gamma\vdash R$, and truth elimination gives $\Gamma\vdash R$. The empty type eliminator translates back to falsehood elimination. These cases exhaust the typing rules for function, product, sum, unit, and empty types, so every typing derivation of $\Gamma^\ast\vdash t:Q^\ast$ determines a natural deduction derivation of $\Gamma\vdash Q$.[/step]

[guided]The converse induction reads the typing rules as proof rules. The only point that needs care is that every type encountered must really be the translation of a proposition. This follows from the hypothesis that the only atomic types in the calculus are the corresponding atomic types in $\mathsf{At}^\ast$: building types with $\to$, $\times$, $+$, $\mathbf{1}$, and $\mathbf{0}$ exactly mirrors building propositions with $\to$, $\wedge$, $\vee$, $\top$, and $\bot$. For example, if the last typing rule is unit elimination, then the term has the form $\operatorname{let}_{\mathbf{1}}(r;c)$ and the premises are \begin{align*} \Gamma^\ast\vdash r:\mathbf{1} \end{align*} and \begin{align*} \Gamma^\ast\vdash c:R^\ast. \end{align*} The type $\mathbf{1}$ is $\top^\ast$, so the induction hypothesis translates the first premise into a derivation of $\Gamma\vdash\top$. The second premise translates into a derivation of $\Gamma\vdash R$. Applying truth elimination in natural deduction gives $\Gamma\vdash R$, which is the proposition corresponding to the conclusion type $R^\ast$.[/guided]

[step:Match beta reductions with local proof reductions] We compare each beta rule with the corresponding introduction-elimination detour in natural deduction. For implication, the beta law is \begin{align*} (\lambda x.u)(a) = u[a/x]. \end{align*} It corresponds to introducing $P\to Q$ from a derivation of $Q$ under assumption $P$, immediately eliminating it with a proof of $P$, and reducing the detour by substituting the proof of $P$ into the derivation of $Q$. For conjunction, the beta laws are \begin{align*} \pi_1((a,b))=a. \end{align*} \begin{align*} \pi_2((a,b))=b. \end{align*} They correspond to introducing $P\wedge Q$ by a pair of proofs and then immediately extracting the left or right component. For disjunction, the beta laws are \begin{align*} \operatorname{case}(\operatorname{inl}(a);x.u;y.v)=u[a/x]. \end{align*} \begin{align*} \operatorname{case}(\operatorname{inr}(b);x.u;y.v)=v[b/y]. \end{align*} They correspond to introducing a disjunction on one side and then immediately performing proof by cases; the active branch is the branch matching the injection. For truth, the unit beta law is \begin{align*} \operatorname{let}_{\mathbf{1}}(\ttstar;c)=c. \end{align*} This corresponds to the local reduction for $\top$: a proof obtained by eliminating the canonical proof of truth reduces to the branch assigned to that proof. For falsehood, there is no introduction rule for $\bot$ and no closed constructor for $\mathbf{0}$. Hence there is no introduction-elimination beta detour for falsehood. Its eliminator corresponds exactly to ex falso reasoning. Thus beta equality in the typed calculus matches local proof reduction in natural deduction for every connective in the fragment. [/step]

[step:Match eta principles with proof expansion principles] The eta laws express that an arbitrary proof or term is determined by its canonical eliminations and reintroductions. For implication, the eta principle is \begin{align*} f = \lambda x.f(x) \end{align*} for $f:P^\ast\to Q^\ast$, with $x:P^\ast$ fresh. This says that a proof of $P\to Q$ is determined by what it does to an arbitrary proof of $P$. For conjunction, the eta principle is \begin{align*} p = (\pi_1(p),\pi_2(p)) \end{align*} for $p:P^\ast\times Q^\ast$. This says that a proof of $P\wedge Q$ is determined by its two projected component proofs. For disjunction, the eta principle says that a term $s:P^\ast+Q^\ast$ is recovered by case analysis using the two injections: \begin{align*} s = \operatorname{case}(s;x.\operatorname{inl}(x);y.\operatorname{inr}(y)). \end{align*} This says that a proof of $P\vee Q$ is determined by eliminating it into the same disjunction and reintroducing the corresponding side. For truth, the eta principle is \begin{align*} u=\ttstar \end{align*} for every $u:\mathbf{1}$. This says that all proofs of $\top$ are equal to the canonical proof. For falsehood, eta is the uniqueness principle for maps out of $\mathbf{0}$: any two eliminations from an empty hypothesis agree because there is no constructor case to distinguish them. Therefore eta equality in the typed calculus matches the usual proof expansion and uniqueness principles in the corresponding natural deduction system. [/step]

[step:Conclude the correspondence] The first induction assigns to every natural deduction derivation of $\Gamma\vdash Q$ a typed lambda term $t$ with \begin{align*} \Gamma^\ast\vdash t:Q^\ast. \end{align*} The second induction assigns to every typing derivation of such a judgment a natural deduction derivation of $\Gamma\vdash Q$. The rule-by-rule beta comparison shows that local proof reductions match computational beta reductions, and the rule-by-rule eta comparison shows that proof expansion principles match eta equalities. Consequently, intuitionistic propositional natural deduction with $\to$, $\wedge$, $\vee$, $\top$, and $\bot$ corresponds to the simply typed lambda calculus with function, product, sum, unit, and empty types, up to the standard beta-eta equivalences. This is precisely the Curry-Howard correspondence for this fragment. [/step]