[proofplan] We define the Curry–Howard term assignment for each natural deduction rule and then compare each principal introduction-elimination detour with the corresponding computation rule. The only structural fact needed is that substituting a proof into a discharged assumption translates to substituting the corresponding term for the corresponding variable. Once the principal detours are checked for implication, conjunction, disjunction, and existential quantification, compatibility of term formation with proof contexts gives the result for reductions occurring inside larger derivations and for finite reduction sequences. [/proofplan]

[step:Define the formulas-as-types translation and the term assignment] Let $\Gamma$ be a finite natural deduction context of the form \begin{align*} \Gamma = A_1, \dots, A_n . \end{align*} Choose distinct variables $x_1, \dots, x_n$, and define the translated typed context $\Gamma^\ast$ by \begin{align*} \Gamma^\ast = x_1 : A_1^\ast, \dots, x_n : A_n^\ast . \end{align*} The type translation $(-)^\ast$ is defined recursively on formulas by \begin{align*} (P)^\ast &= P^\ast &&\text{for each atomic formula } P, \\ (A \to B)^\ast &= A^\ast \to B^\ast, \\ (A \wedge B)^\ast &= A^\ast \times B^\ast, \\ (A \vee B)^\ast &= A^\ast + B^\ast, \\ (\exists z \in S\, A(z))^\ast &= \Sigma_{z:S} A(z)^\ast . \end{align*} Here $P^\ast$ is the atomic type corresponding to the atomic formula $P$, $A^\ast \times B^\ast$ is the product type, $A^\ast + B^\ast$ is the sum type, and $\Sigma_{z:S} A(z)^\ast$ is the dependent pair type. For each derivation $\mathcal D$ of $\Gamma \vdash A$, define a term assignment \begin{align*} \mathcal T: \{\text{derivations } \mathcal D \text{ of } \Gamma \vdash A\} &\to \{\text{typed terms } t \text{ with } \Gamma^\ast \vdash t : A^\ast\} \\ \mathcal D &\mapsto t_{\mathcal D} \end{align*} recursively by the natural deduction rule used last in $\mathcal D$. An assumption $A_i$ is assigned the variable $x_i$. Implication introduction sends a derivation of $\Gamma, A \vdash B$ with assigned term $u$ to $\lambda x:A^\ast.\,u$, and implication elimination sends terms $f:A^\ast \to B^\ast$ and $a:A^\ast$ to $f\,a$. Conjunction introduction sends $a:A^\ast$ and $b:B^\ast$ to $(a,b)$, while conjunction eliminations send $p:A^\ast \times B^\ast$ to $\pi_1(p)$ and $\pi_2(p)$. Disjunction introductions send $a:A^\ast$ to $\operatorname{inl}(a):A^\ast+B^\ast$ and $b:B^\ast$ to $\operatorname{inr}(b):A^\ast+B^\ast$, while [disjunction elimination](/theorems/4625) sends a sum term $s:A^\ast+B^\ast$ and branch terms $u:C^\ast$ and $v:C^\ast$ to $\operatorname{case}(s; x.u; y.v)$. Existential introduction sends a witness $w:S$ and a proof term $a:A(w)^\ast$ to $(w,a):\Sigma_{z:S}A(z)^\ast$, and existential elimination sends a dependent pair $p:\Sigma_{z:S}A(z)^\ast$ and a branch term $u:C^\ast$ depending on $z:S$ and $x:A(z)^\ast$ to $\operatorname{let}(z,x)=p\operatorname{ in }u$. [/step]

[step:Relate proof substitution to term substitution]Suppose $\mathcal E$ is a derivation of $\Gamma \vdash A$ and $\mathcal F$ is a derivation of $\Gamma, A \vdash B$. Let $\mathcal F[\mathcal E/A]$ denote the derivation of $\Gamma \vdash B$ obtained by replacing each open use of the distinguished assumption $A$ in $\mathcal F$ by the derivation $\mathcal E$. If $x:A^\ast$ is the variable assigned to that distinguished assumption, then the assigned term satisfies \begin{align*} t_{\mathcal F[\mathcal E/A]} = t_{\mathcal F}[t_{\mathcal E}/x] \end{align*} up to alpha-equivalence of bound variables. This is proved by induction on the last rule of $\mathcal F$. If $\mathcal F$ is the distinguished assumption $A$, then $\mathcal F[\mathcal E/A]=\mathcal E$, and the equality is \begin{align*} t_{\mathcal E}=x[t_{\mathcal E}/x]. \end{align*} If $\mathcal F$ is a different assumption, then the substitution does not change the proof, and the corresponding variable is not $x$. For each introduction or elimination rule, the proof substitution is performed recursively in the immediate subderivations, and the term assignment is defined by applying the matching term constructor to the recursively assigned terms. The induction hypothesis therefore gives the required equality after applying the same constructor on both sides. Bound variables are renamed before substitution when necessary, so the equality is understood up to alpha-equivalence. We also record the object-substitution compatibility needed for existential elimination. Let $w:S$ be a term, and let $\mathcal F$ be a derivation of $\Gamma,z:S,A(z) \vdash C$ in which $z$ is an eigenvariable fresh for $\Gamma$ and not free in $C$. Let $\mathcal F[w/z]$ denote the capture-avoiding substitution of $w$ for $z$ in formulas, assumptions, and terms of the derivation. Formula translation commutes with this substitution, \begin{align*} (A(z)[w/z])^\ast = A(z)^\ast[w/z], \end{align*} by structural induction on formulas. A simultaneous induction on the last rule of $\mathcal F$ then gives \begin{align*} t_{\mathcal F[w/z]} = t_{\mathcal F}[w/z] \end{align*} up to alpha-equivalence. The eigenvariable condition ensures that substituting $w$ for $z$ does not change the ambient context $\Gamma$ or the conclusion $C$, and capture-avoidance is achieved by renaming bound variables before substitution.[/step]

[guided]The point of this step is to justify the main syntactic move used in every beta-reduction case. A local proof reduction removes an introduction followed immediately by an elimination, and the result is obtained by inserting the proof of the introduced premise into the place where the eliminated assumption was used. The term-level version of that operation is ordinary substitution of a term for a variable. Formally, let $\mathcal E$ be a derivation of $\Gamma \vdash A$, and let $\mathcal F$ be a derivation of $\Gamma,A \vdash B$. The distinguished assumption $A$ is represented in the translated context by a variable $x:A^\ast$. Replacing the distinguished assumption in $\mathcal F$ by the proof $\mathcal E$ gives a derivation $\mathcal F[\mathcal E/A]$ of $\Gamma \vdash B$. We prove \begin{align*} t_{\mathcal F[\mathcal E/A]} = t_{\mathcal F}[t_{\mathcal E}/x] \end{align*} by induction on the construction of $\mathcal F$. If $\mathcal F$ is exactly the distinguished assumption $A$, then the proof substitution gives $\mathcal E$. Its assigned term is $t_{\mathcal E}$. The assigned term of the distinguished assumption is $x$, and term substitution gives $x[t_{\mathcal E}/x]=t_{\mathcal E}$. If $\mathcal F$ is an assumption different from the distinguished assumption, then proof substitution leaves it unchanged. Its assigned variable is some $y$ with $y \ne x$, and term substitution gives $y[t_{\mathcal E}/x]=y$. For an introduction or elimination rule, the derivation $\mathcal F$ is built from one or more immediate subderivations. Proof substitution acts on those subderivations, while the Curry–Howard assignment applies the corresponding term constructor after translating the subderivations. The induction hypothesis identifies each translated substituted subderivation with the corresponding term substitution. Applying the same constructor preserves equality. Whenever a constructor binds a variable, such as $\lambda x:A^\ast.\,u$, $\operatorname{case}(s;x.u;y.v)$, or $\operatorname{let}(z,x)=p\operatorname{ in }u$, bound variables are first renamed to avoid capture. Thus the equality holds up to alpha-equivalence. The existential case also requires substitution of an object witness for an eigenvariable, not only substitution of a proof for a formula assumption. Let $w:S$ be a term, and let $\mathcal F$ be a derivation of $\Gamma,z:S,A(z) \vdash C$. In existential elimination, the variable $z:S$ is an eigenvariable: it is fresh for the ambient context $\Gamma$ and does not occur free in the conclusion $C$. These side conditions are what allow the reduced derivation to remain a derivation over $\Gamma$ with conclusion $C$ after the witness is substituted. Write $\mathcal F[w/z]$ for the derivation obtained by capture-avoiding substitution of $w$ for $z$ throughout formulas, assumptions, and term annotations in $\mathcal F$. First, the formulas-as-types translation is compatible with this substitution. For every formula $A(z)$, structural induction on $A$ gives \begin{align*} (A(z)[w/z])^\ast = A(z)^\ast[w/z]. \end{align*} For atomic formulas this is the definition of the translation on atomic predicates. The implication, conjunction, and disjunction cases follow because translation is defined recursively by the corresponding type formers. In the existential case, bound variables are renamed before substitution if necessary, so substitution is capture-avoiding and commutes with the dependent pair type former. Now we prove the corresponding statement for derivations. A simultaneous induction on the construction of $\mathcal F$ gives \begin{align*} t_{\mathcal F[w/z]} = t_{\mathcal F}[w/z] \end{align*} up to alpha-equivalence. In an assumption case, the previous formula-substitution compatibility identifies the substituted assumption type with the substituted translated type. In each introduction or elimination case, object substitution acts recursively on the immediate subderivations, and the term assignment then applies the same constructor as before. The induction hypothesis identifies the translated substituted subderivations with the corresponding object substitutions in their assigned terms. Constructors with binders are handled after renaming bound variables away from the free variables of $w$, so no variable capture occurs.[/guided]

[step:Check the implication detour as beta-reduction] Let $\mathcal E$ be a derivation of $\Gamma \vdash A$, and let $\mathcal F$ be a derivation of $\Gamma,A \vdash B$. The implication introduction applied to $\mathcal F$ translates to $\lambda x:A^\ast.\,t_{\mathcal F}$, and eliminating it with $\mathcal E$ translates to \begin{align*} (\lambda x:A^\ast.\,t_{\mathcal F})\,t_{\mathcal E}. \end{align*} The computation rule for function application gives \begin{align*} (\lambda x:A^\ast.\,t_{\mathcal F})\,t_{\mathcal E} \longrightarrow t_{\mathcal F}[t_{\mathcal E}/x]. \end{align*} By the substitution step, \begin{align*} t_{\mathcal F}[t_{\mathcal E}/x] = t_{\mathcal F[\mathcal E/A]}. \end{align*} The reduced proof is exactly $\mathcal F[\mathcal E/A]$, so the implication detour translates to the corresponding beta-reduction. [/step]

[step:Check the conjunction detours as projection reductions] Let $\mathcal E_1$ be a derivation of $\Gamma \vdash A$, and let $\mathcal E_2$ be a derivation of $\Gamma \vdash B$. Conjunction introduction translates to the pair \begin{align*} (t_{\mathcal E_1},t_{\mathcal E_2}) : A^\ast \times B^\ast . \end{align*} The first conjunction elimination translates to \begin{align*} \pi_1(t_{\mathcal E_1},t_{\mathcal E_2}), \end{align*} and the product computation rule gives \begin{align*} \pi_1(t_{\mathcal E_1},t_{\mathcal E_2}) \longrightarrow t_{\mathcal E_1}. \end{align*} The local proof reduction for this detour removes the pair introduction and keeps the left derivation $\mathcal E_1$, whose assigned term is $t_{\mathcal E_1}$. Hence the first conjunction detour translates to the first projection reduction. The second conjunction elimination translates to \begin{align*} \pi_2(t_{\mathcal E_1},t_{\mathcal E_2}), \end{align*} and the product computation rule gives \begin{align*} \pi_2(t_{\mathcal E_1},t_{\mathcal E_2}) \longrightarrow t_{\mathcal E_2}. \end{align*} The local proof reduction keeps the right derivation $\mathcal E_2$, so the second conjunction detour translates to the second projection reduction. [/step]

[step:Check the disjunction detours as case reductions] Let $\mathcal E$ be a derivation of $\Gamma \vdash A$. Let $\mathcal F$ be a derivation of $\Gamma,A \vdash C$, with the distinguished assumption $A$ represented by $x:A^\ast$. Let $\mathcal G$ be a derivation of $\Gamma,B \vdash C$, with the distinguished assumption $B$ represented by $y:B^\ast$. The left disjunction introduction followed by disjunction elimination translates to \begin{align*} \operatorname{case}(\operatorname{inl}(t_{\mathcal E}); x.t_{\mathcal F}; y.t_{\mathcal G}). \end{align*} The sum computation rule gives \begin{align*} \operatorname{case}(\operatorname{inl}(t_{\mathcal E}); x.t_{\mathcal F}; y.t_{\mathcal G}) \longrightarrow t_{\mathcal F}[t_{\mathcal E}/x]. \end{align*} By the substitution step, \begin{align*} t_{\mathcal F}[t_{\mathcal E}/x] = t_{\mathcal F[\mathcal E/A]}. \end{align*} The local proof reduction for the left injection selects the left branch and substitutes $\mathcal E$ for its open assumption, so the translated reduction is the left case computation rule. Now let $\mathcal E'$ be a derivation of $\Gamma \vdash B$. The right disjunction introduction followed by disjunction elimination translates to \begin{align*} \operatorname{case}(\operatorname{inr}(t_{\mathcal E'}); x.t_{\mathcal F}; y.t_{\mathcal G}). \end{align*} The sum computation rule gives \begin{align*} \operatorname{case}(\operatorname{inr}(t_{\mathcal E'}); x.t_{\mathcal F}; y.t_{\mathcal G}) \longrightarrow t_{\mathcal G}[t_{\mathcal E'}/y]. \end{align*} By the substitution step, \begin{align*} t_{\mathcal G}[t_{\mathcal E'}/y] = t_{\mathcal G[\mathcal E'/B]}. \end{align*} The local proof reduction for the right injection selects the right branch and substitutes $\mathcal E'$ for its open assumption, so the translated reduction is the right case computation rule. [/step]

[step:Check the existential detour as dependent pair elimination] Let $w:S$ be a witness term, let $\mathcal E$ be a derivation of $\Gamma \vdash A(w)$, and let $\mathcal F$ be a derivation of $\Gamma,z:S,A(z) \vdash C$, where the witness variable is $z:S$ and the proof variable is $x:A(z)^\ast$. Existential introduction translates to \begin{align*} (w,t_{\mathcal E}) : \Sigma_{z:S}A(z)^\ast . \end{align*} Eliminating this existential proof translates to \begin{align*} \operatorname{let}(z,x)=(w,t_{\mathcal E})\operatorname{ in }t_{\mathcal F}. \end{align*} The dependent pair computation rule gives \begin{align*} \operatorname{let}(z,x)=(w,t_{\mathcal E})\operatorname{ in }t_{\mathcal F} \longrightarrow t_{\mathcal F}[w/z][t_{\mathcal E}/x]. \end{align*} The local proof reduction for existential introduction followed by existential elimination first performs capture-avoiding witness substitution $w$ for the eigenvariable $z$, producing a derivation $\mathcal F[w/z]$ of $\Gamma,A(w) \vdash C$. The eigenvariable side condition for existential elimination gives that $z$ is fresh for $\Gamma$ and not free in $C$, so this substitution changes neither the ambient context nor the conclusion. The object-substitution compatibility proved above gives \begin{align*} t_{\mathcal F[w/z]} = t_{\mathcal F}[w/z] \end{align*} up to alpha-equivalence. The reduced proof then substitutes the derivation $\mathcal E$ for the open proof assumption $A(w)$ in $\mathcal F[w/z]$. Applying the proof-substitution compatibility with proof variable $x:A(w)^\ast$ gives \begin{align*} t_{(\mathcal F[w/z])[\mathcal E/A(w)]} = t_{\mathcal F[w/z]}[t_{\mathcal E}/x] = t_{\mathcal F}[w/z][t_{\mathcal E}/x]. \end{align*} This is exactly the term produced by the dependent pair computation rule, so the existential detour translates to that computation rule. [/step]

[step:Extend the principal checks to arbitrary local reductions and finite sequences] Let $\mathcal C[-]$ be a one-hole derivation context, meaning a derivation with one distinguished subderivation omitted. Let $\mathcal D_0$ be a principal introduction-elimination detour and let $\mathcal D_0'$ be its local reduction. The previous steps show that \begin{align*} t_{\mathcal D_0} \longrightarrow t_{\mathcal D_0'}. \end{align*} Because the term assignment is recursive on derivations, there is a corresponding one-hole term context $C[-]$ such that \begin{align*} t_{\mathcal C[\mathcal D_0]} &= C[t_{\mathcal D_0}], \\ t_{\mathcal C[\mathcal D_0']} &= C[t_{\mathcal D_0'}]. \end{align*} The computation relation in $\Lambda_{\iota}$ is closed under term contexts, so \begin{align*} C[t_{\mathcal D_0}] \longrightarrow C[t_{\mathcal D_0'}]. \end{align*} Therefore every local proof reduction $\mathcal D \rightsquigarrow \mathcal D'$ translates to a computation reduction \begin{align*} t_{\mathcal D} \longrightarrow t_{\mathcal D'}. \end{align*} If \begin{align*} \mathcal D_0 \rightsquigarrow \mathcal D_1 \rightsquigarrow \cdots \rightsquigarrow \mathcal D_m \end{align*} is a finite sequence of local proof reductions, applying the one-step result to each adjacent pair gives \begin{align*} t_{\mathcal D_0} \longrightarrow t_{\mathcal D_1} \longrightarrow \cdots \longrightarrow t_{\mathcal D_m}. \end{align*} This proves that local normalization reductions in intuitionistic natural deduction correspond exactly to the associated computation rules under the Curry–Howard translation. [/step]