[proofplan] We define a one-step reduction relation on derivations by contracting each local detour: an introduction rule immediately followed by the matching elimination rule. Each contraction preserves the conclusion and does not introduce any undischarged assumption outside the original context, because it only substitutes derivations for discharged assumption occurrences or selects an already present subderivation. To prove that repeated contraction terminates, we translate derivations into typed terms in the [simply typed lambda calculus](/page/Simply%20Typed%20Lambda%20Calculus) with products, sums, function types, and empty type, using assumption classes so discharged occurrences are represented by the correct bound variables. Local-detour contraction translates to beta-reduction, so strong normalization of the target calculus forbids an infinite contraction sequence. A terminal derivation has no remaining local detours, hence is normal in the beta-normal sense stated in the theorem. [/proofplan] [step:Define formula complexity and local detours] Define the complexity map $c$ from formulas to $\mathbb N$ recursively by \begin{align*} c(P) &= 0,\\ c(\bot) &= 0,\\ c(B \land C) &= 1 + c(B) + c(C),\\ c(B \lor C) &= 1 + c(B) + c(C),\\ c(B \to C) &= 1 + c(B) + c(C), \end{align*} where $P$ is a propositional variable and $B,C$ are formulas. A local detour in a derivation is a formula occurrence $F$ such that $F$ is the conclusion of an introduction rule and is also the major premise of the corresponding elimination rule. Its degree is $c(F)$. A derivation is called normal, in the beta-normal sense used in this theorem, if it contains no local detour. A derivation is terminal for the one-step contraction relation if no contraction described below applies to it; equivalently, by the displayed list of possible detours, it contains no local detour. Thus the possible local detours are the following. For conjunction, the derivation has one of the two forms \begin{align*} \frac{ \frac{\mathcal D_1 \quad \mathcal D_2}{B \land C}\land I }{B}\land E_1, \qquad \frac{ \frac{\mathcal D_1 \quad \mathcal D_2}{B \land C}\land I }{C}\land E_2. \end{align*} For implication, the derivation has the form \begin{align*} \frac{ \frac{\mathcal E}{B \to C}\to I \quad \mathcal D_0 }{C}\to E, \end{align*} where the displayed $\to I$ discharges some occurrences of the assumption $B$ in $\mathcal E$. For disjunction, let $D$ be a formula denoting the common conclusion of the two case derivations in the disjunction-elimination rule. The derivation has one of the two forms \begin{align*} \frac{ \frac{\mathcal D_0}{B \lor C}\lor I_1 \quad \mathcal E_1 \quad \mathcal E_2 }{D}\lor E, \qquad \frac{ \frac{\mathcal D_0}{B \lor C}\lor I_2 \quad \mathcal E_1 \quad \mathcal E_2 }{D}\lor E, \end{align*} where the left case derivation $\mathcal E_1$ discharges occurrences of $B$, and the right case derivation $\mathcal E_2$ discharges occurrences of $C$. There is no corresponding local detour for $\bot$, since $\bot$ has no introduction rule in $\mathsf{NJ}_{\mathrm{prop}}$. [/step] [step:Contract conjunction detours by projection] A conjunction detour is reduced by replacing the whole detour with the selected premise derivation: \begin{align*} \frac{ \frac{\mathcal D_1 \quad \mathcal D_2}{B \land C}\land I }{B}\land E_1 \quad\rightsquigarrow\quad \mathcal D_1, \end{align*} and \begin{align*} \frac{ \frac{\mathcal D_1 \quad \mathcal D_2}{B \land C}\land I }{C}\land E_2 \quad\rightsquigarrow\quad \mathcal D_2. \end{align*} The conclusion is preserved, since the first reduced derivation concludes $B$ and the second concludes $C$. The undischarged assumptions of the selected subderivation are among the undischarged assumptions of the original conjunction detour, so no new open assumption is introduced. [/step] [step:Contract implication detours by derivation substitution] Consider an implication detour \begin{align*} \frac{ \frac{\mathcal E}{B \to C}\to I \quad \mathcal D_0 }{C}\to E, \end{align*} where $\mathcal D_0$ concludes $B$, and where the displayed implication introduction discharges a finite set of assumption occurrences of formula $B$ in $\mathcal E$. Define $\mathcal E[\mathcal D_0/B]$ to be the derivation obtained from $\mathcal E$ by replacing each discharged occurrence of the assumption $B$ by a fresh copy of the derivation $\mathcal D_0$. Then the reduction is \begin{align*} \frac{ \frac{\mathcal E}{B \to C}\to I \quad \mathcal D_0 }{C}\to E \quad\rightsquigarrow\quad \mathcal E[\mathcal D_0/B]. \end{align*} This replacement is a valid derivation of $C$. Indeed, every inference rule in $\mathcal E$ remains an instance of the same rule after the replacement, and every replaced leaf has conclusion $B$, which is exactly the formula required at the discharged assumption occurrence. The undischarged assumptions of $\mathcal E[\mathcal D_0/B]$ are the undischarged assumptions of $\mathcal E$ not discharged by the displayed $\to I$, together with the undischarged assumptions of the inserted copies of $\mathcal D_0$. These are precisely assumptions already open in the original implication-elimination derivation. Hence the reduction preserves both the conclusion and containment of open assumptions in $\Gamma$. [guided] The only delicate point in the implication case is discharged assumptions. The derivation $\mathcal E$ proves $C$ under some temporary assumptions of formula $B$, and the introduction rule turns that conditional derivation into a derivation of $B \to C$ by discharging exactly those temporary occurrences of $B$. If we then immediately apply the implication to a derivation $\mathcal D_0$ of $B$, the detour has done no real work: the correct reduced derivation is obtained by feeding $\mathcal D_0$ directly into every discharged use of $B$. Formally, let $\mathcal E[\mathcal D_0/B]$ denote the derivation obtained by replacing each discharged assumption occurrence of $B$ in $\mathcal E$ by a fresh copy of $\mathcal D_0$. This replacement is well-typed as a derivation operation because every replaced leaf had conclusion $B$, and $\mathcal D_0$ also has conclusion $B$. All inference rules above those leaves are unchanged, so the resulting tree remains a valid natural deduction derivation. Its conclusion is still $C$, because the root of $\mathcal E$ was $C$ and the root rule is not changed. Now consider open assumptions. The assumptions of $\mathcal E$ that were discharged by the displayed $\to I$ are no longer open, because they have been replaced. The open assumptions contributed by the inserted copies of $\mathcal D_0$ are exactly assumptions already open in the original application of $\to E$. Therefore the reduced derivation has no undischarged assumption outside the original set of undischarged assumptions. In particular, if the original derivation had all open assumptions contained in $\Gamma$, then so does the reduced derivation. [/guided] [/step] [step:Contract disjunction detours by selecting the introduced case] For a left disjunction detour, \begin{align*} \frac{ \frac{\mathcal D_0}{B \lor C}\lor I_1 \quad \mathcal E_1 \quad \mathcal E_2 }{D}\lor E, \end{align*} where $\mathcal E_1$ is a derivation of $D$ from a discharged assumption occurrence, or discharged assumption occurrences, of $B$, define $\mathcal E_1[\mathcal D_0/B]$ by replacing those discharged occurrences of $B$ by fresh copies of $\mathcal D_0$. The reduction is \begin{align*} \frac{ \frac{\mathcal D_0}{B \lor C}\lor I_1 \quad \mathcal E_1 \quad \mathcal E_2 }{D}\lor E \quad\rightsquigarrow\quad \mathcal E_1[\mathcal D_0/B]. \end{align*} For a right disjunction detour, \begin{align*} \frac{ \frac{\mathcal D_0}{B \lor C}\lor I_2 \quad \mathcal E_1 \quad \mathcal E_2 }{D}\lor E, \end{align*} where $\mathcal E_2$ is a derivation of $D$ from discharged assumption occurrences of $C$, define $\mathcal E_2[\mathcal D_0/C]$ analogously. The reduction is \begin{align*} \frac{ \frac{\mathcal D_0}{B \lor C}\lor I_2 \quad \mathcal E_1 \quad \mathcal E_2 }{D}\lor E \quad\rightsquigarrow\quad \mathcal E_2[\mathcal D_0/C]. \end{align*} In each case the conclusion remains $D$. The replacement only substitutes a derivation of the introduced disjunct for discharged assumptions of that same disjunct, so the resulting tree is a valid derivation. Its undischarged assumptions are among the undischarged assumptions of the original disjunction-elimination derivation. [guided] [Disjunction elimination](/theorems/4625) is a case-analysis rule. If the major premise $B \lor C$ was itself obtained by introducing the left disjunct from a derivation of $B$, then the right case is irrelevant: the proof should continue directly with the left case proof, using the actual derivation of $B$. This is exactly the replacement $\mathcal E_1[\mathcal D_0/B]$. The well-formedness check is the same substitution check as in the implication case. The derivation $\mathcal E_1$ concludes $D$ under temporary assumptions of formula $B$. Replacing each discharged temporary assumption $B$ by a fresh copy of $\mathcal D_0$, which also concludes $B$, preserves every inference rule above the leaves. Hence $\mathcal E_1[\mathcal D_0/B]$ is a derivation of $D$. For the right introduction case, replace each discharged temporary assumption occurrence of $C$ in $\mathcal E_2$ by a fresh copy of $\mathcal D_0$. Each replaced leaf and each inserted copy has conclusion $C$, so every inference rule above those leaves remains a valid instance of its original natural deduction rule, and the resulting derivation concludes $D$. In both cases, the open assumptions of the reduced derivation are exactly the non-discharged assumptions already present in the selected case derivation, together with the open assumptions of the inserted derivation $\mathcal D_0$. These assumptions were already open in the original derivation using $\lor E$, so containment in $\Gamma$ is preserved. [/guided] [/step] [step:Show that contraction preserves derivability from the context] Let $\mathcal R$ be any one-step contraction described above, and suppose $\mathcal R$ transforms a derivation $\mathcal D$ into a derivation $\mathcal D_1$. We prove that $\mathcal D_1$ has the same conclusion as $\mathcal D$ and that every undischarged assumption of $\mathcal D_1$ is an undischarged assumption of $\mathcal D$. For conjunction contractions, this follows because the reduced derivation is one of the two immediate premise derivations of the conjunction introduction. For implication and disjunction contractions, it follows from the substitution construction: each inserted derivation has the same conclusion as the discharged assumption occurrence it replaces, and every open assumption introduced by an inserted copy was already open in the original elimination derivation. Therefore, if the open assumptions of $\mathcal D$ are contained in $\Gamma$, then the open assumptions of $\mathcal D_1$ are also contained in $\Gamma$. By induction on the length of a finite sequence of contractions, every finite reduction sequence beginning with $\mathcal D$ preserves the final conclusion $A$ and preserves containment of undischarged assumptions in $\Gamma$. [/step] [step:Translate formulas and assumption classes into typed terms] Let $\Lambda$ be the [simply typed lambda calculus](/page/Simply%20Typed%20Lambda%20Calculus) with product types, sum types, function types, and empty type. Define the formula-to-type map $(-)^\ast$ from propositional formulas to simple types by sending each propositional variable $P$ to a base type $P^\ast$, sending $\bot$ to the empty type $0$, and recursively setting \begin{align*} (B \land C)^\ast &= B^\ast \times C^\ast,\\ (B \lor C)^\ast &= B^\ast + C^\ast,\\ (B \to C)^\ast &= B^\ast \to C^\ast. \end{align*} An assumption class means either one undischarged assumption occurrence or one finite family of assumption occurrences discharged by a single introduction or elimination rule. Assign one typed variable $x_\alpha : F_\alpha^\ast$ to each active assumption class $\alpha$ of formula $F_\alpha$. Thus several occurrences of the same temporary assumption discharged together are represented by the same variable, while distinct undischarged assumption occurrences may still have distinct variables. By induction on the last rule of a natural deduction derivation $\mathcal E$, define a typed term $t_{\mathcal E}$ whose type is the translation of the conclusion of $\mathcal E$. Conjunction introduction is translated as pairing, conjunction elimination as projection, implication elimination as application, disjunction introduction as the corresponding coproduct injection, disjunction elimination as case analysis, and $\bot E$ as the eliminator from $0$. If $\mathcal E$ ends in $\to I$ and discharges the assumption class $\alpha$ of formula $B$, then the induction hypothesis gives a term $u$ of type $C^\ast$ in a context containing the single variable $x_\alpha : B^\ast$, and the translated term is $\lambda x_\alpha:B^\ast. u$ of type $B^\ast \to C^\ast$. If $\mathcal E$ ends in $\lor E$, then the two case derivations are translated in contexts containing the branch variables for their discharged assumption classes, and the translated term is the corresponding case term. [guided] The point of using assumption classes is to match the binding structure of natural deduction. An implication introduction may discharge many occurrences of $B$, but those occurrences form one temporary hypothesis class. Therefore the typed translation must bind one variable $x_\alpha : B^\ast$, and every discharged occurrence in that class translates to that same variable. Define $\Lambda$ to be the simply typed lambda calculus with product types, sum types, function types, and empty type. The formula-to-type map $(-)^\ast$ is \begin{align*} (B \land C)^\ast &= B^\ast \times C^\ast,\\ (B \lor C)^\ast &= B^\ast + C^\ast,\\ (B \to C)^\ast &= B^\ast \to C^\ast, \end{align*} with propositional variables sent to base types and $\bot$ sent to $0$. For every active assumption class $\alpha$ of formula $F_\alpha$, introduce one variable $x_\alpha : F_\alpha^\ast$. This convention is what prevents the translation from producing a malformed abstraction over several independent variables when the proof rule discharges one hypothesis class. The translation of rules is then defined by induction on the derivation. Pair introduction, projections, application, injections, case analysis, and the empty-type eliminator are the standard typed constructors. For implication introduction, if a derivation of $C$ uses the temporary assumption class $\alpha$ of formula $B$, then the induction hypothesis produces a term $u:C^\ast$ in a context containing $x_\alpha:B^\ast$. Abstracting over that one variable gives $\lambda x_\alpha:B^\ast.u : B^\ast \to C^\ast$, which has exactly the type corresponding to $B \to C$. Thus the typing induction is well-defined and assigns to every derivation $\mathcal E$ a term $t_{\mathcal E}$ of type $F^\ast$ when $\mathcal E$ concludes $F$. [/guided] [/step] [step:Identify proof contractions with beta-reductions] A beta-reduction in $\Lambda$ is one of the computation rules for eliminating a constructor immediately after introducing it: projecting a pair, applying a lambda abstraction to an argument, or performing case analysis on an injected summand. Under the translation above, each conjunction contraction becomes a product beta-reduction, each implication contraction becomes a function beta-reduction, and each disjunction contraction becomes a sum beta-reduction. For implication and disjunction, the derivation substitution operation is translated as capture-avoiding substitution of typed terms. In the implication case, replacing every discharged occurrence in the assumption class $\alpha$ by a fresh copy of $\mathcal D_0$ translates to substituting $t_{\mathcal D_0}$ for the single bound variable $x_\alpha$. The same argument applies to the selected branch in the disjunction case. Hence an infinite sequence of proof contractions starting from $\mathcal D$ would translate to an infinite beta-reduction sequence starting from $t_{\mathcal D}$. [guided] We now check that the syntactic contraction of proofs is not merely analogous to beta-reduction; it is exactly beta-reduction after translation. A conjunction detour translates to a projection applied to a pair, so contraction corresponds to the product beta-rule. An implication detour translates to an application $(\lambda x_\alpha:B^\ast.u)\,v$, where $v=t_{\mathcal D_0}$, so contraction corresponds to replacing the bound variable $x_\alpha$ by $v$ in $u$. This is where the assumption-class convention matters again. The discharged occurrences of $B$ are all represented by the one variable $x_\alpha$, so replacing those occurrences in the derivation translates exactly to capture-avoiding substitution $u[v/x_\alpha]$. For disjunction, a case expression whose scrutinee is a left injection reduces to the left branch with the injected term substituted for the left branch variable, and the right injection case is identical with the right branch variable. Therefore every one-step proof contraction gives one beta-reduction of the translated typed term. An infinite contraction sequence would consequently give an infinite beta-reduction sequence from $t_{\mathcal D}$. [/guided] [/step] [step:Apply strong normalization to rule out infinite contraction sequences] We use the [Strong Normalization for Simply Typed Lambda Calculus](/page/Strong%20Normalization%20for%20Simply%20Typed%20Lambda%20Calculus): every well-typed term in the simply typed lambda calculus with products, sums, function types, and empty type admits no infinite beta-reduction sequence. This result applies to $t_{\mathcal D}$ because the preceding typing induction constructs $t_{\mathcal D}$ as a well-typed term of type $A^\ast$ in the context obtained from the open assumption classes of $\mathcal D$. Therefore no infinite contraction sequence can begin at $\mathcal D$, and repeated contraction from $\mathcal D$ terminates after finitely many steps. [guided] The final termination input is strong normalization. The theorem says that if a term is well typed in the simply typed lambda calculus with products, sums, function types, and empty type, then there is no infinite sequence of beta-reductions beginning with that term. The translation step verifies the required hypothesis for the particular term $t_{\mathcal D}$: it is well typed, its type is $A^\ast$, and its free variables correspond exactly to the open assumption classes of $\mathcal D$. If there were an infinite sequence of local-detour contractions beginning with $\mathcal D$, the previous step would translate it into an infinite beta-reduction sequence beginning with $t_{\mathcal D}$. Strong normalization forbids such a sequence. Hence every contraction sequence from $\mathcal D$ is finite, so the process of repeatedly contracting local detours must eventually stop. [/guided] [/step] [step:Take the terminal derivation as the required normal derivation] Beginning with $\mathcal D$, repeatedly contract any local detour whenever one exists. By the termination step, this process stops after finitely many contractions. Let the terminal derivation be $\mathcal D'$. By preservation under contraction, $\mathcal D'$ has conclusion $A$, and every undischarged assumption of $\mathcal D'$ is contained in $\Gamma$. Since the process stops exactly when no local detour remains, no formula occurrence in $\mathcal D'$ is both the conclusion of an introduction rule and the major premise of the matching elimination rule. By the definition of normal derivation used in the theorem statement, $\mathcal D'$ is normal. This proves the theorem. [/step]