[proofplan] We prove the intuitionistic equivalence by two inductions on derivation trees. A natural-deduction derivation is translated into an $\mathrm{LJ}$ derivation by reading introduction rules as right rules and elimination rules as left rules together with cut. Conversely, an $\mathrm{LJ}$ derivation is translated into natural deduction by reading right rules as introductions, left rules as eliminations or case analyses, and cut as substitution of a derivation for an open assumption. The classical equivalence is obtained by replacing a finite succedent $\Delta$ with the single formula $\bigvee \Delta$ and checking, again by induction on derivations, that the $\mathrm{LK}$ right and left rules are exactly the classical natural-deduction rules for reasoning with a finite disjunction of alternatives. [/proofplan] [step:Fix the derivability relations and the structural conventions] We treat contexts as finite lists of formulas. The structural rules exchange, weakening, and contraction are available in the sequent calculi, and the corresponding operations on open assumptions are available in natural deduction: assumptions may be reordered, unused, and used more than once. Thus a derivation from $\Gamma$ depends only on the finite multiset of open assumptions represented by $\Gamma$. For intuitionistic sequents, the succedent contains exactly one formula. For classical sequents, the succedent is a finite list of formulas. The cut rules used below are: \begin{align*} \frac{\Gamma \Rightarrow A \qquad \Gamma,A \Rightarrow B}{\Gamma \Rightarrow B} \quad \text{in } \mathrm{LJ}, \end{align*} and \begin{align*} \frac{\Gamma \Rightarrow \Delta,A \qquad \Gamma,A \Rightarrow \Delta}{\Gamma \Rightarrow \Delta} \quad \text{in } \mathrm{LK}, \end{align*} with harmless variants obtained by exchange and weakening. [/step] [step:Translate intuitionistic natural deduction derivations into $\mathrm{LJ}$ derivations] We prove, by induction on an $\mathrm{NJ}$ derivation $\mathcal{D}$ of $\Gamma \vdash_{\mathrm{NJ}} A$, that $\Gamma \Rightarrow A$ is derivable in $\mathrm{LJ}$. If $\mathcal{D}$ is an open assumption $A \in \Gamma$, then $\Gamma \Rightarrow A$ follows from the identity axiom $A \Rightarrow A$ by weakening and exchange. For conjunction introduction, suppose the last rule derives $A \wedge B$ from derivations of $\Gamma \vdash_{\mathrm{NJ}} A$ and $\Gamma \vdash_{\mathrm{NJ}} B$. By the induction hypothesis there are $\mathrm{LJ}$ derivations of $\Gamma \Rightarrow A$ and $\Gamma \Rightarrow B$. Applying the right rule for $\wedge$ gives \begin{align*} \frac{\Gamma \Rightarrow A \qquad \Gamma \Rightarrow B}{\Gamma \Rightarrow A \wedge B}. \end{align*} For conjunction elimination, suppose the last rule derives $A$ from $\Gamma \vdash_{\mathrm{NJ}} A \wedge B$. The induction hypothesis gives $\Gamma \Rightarrow A \wedge B$. The left rule for $\wedge$ gives $A \wedge B \Rightarrow A$ from the identity axiom $A \Rightarrow A$. Cutting these two sequents gives $\Gamma \Rightarrow A$. The second projection is identical with $B$ in place of $A$. For implication introduction, suppose the last rule discharges an assumption $A$ and derives $B$ from $\Gamma,A$. The induction hypothesis gives $\Gamma,A \Rightarrow B$. Applying the right rule for $\to$ gives \begin{align*} \Gamma \Rightarrow A \to B. \end{align*} For implication elimination, suppose the last rule is modus ponens, deriving $B$ from derivations of $\Gamma \vdash_{\mathrm{NJ}} A \to B$ and $\Gamma \vdash_{\mathrm{NJ}} A$. By induction, $\Gamma \Rightarrow A \to B$ and $\Gamma \Rightarrow A$ are derivable. The left rule for $\to$ yields \begin{align*} \frac{\Gamma \Rightarrow A \qquad B \Rightarrow B}{\Gamma,A \to B \Rightarrow B}. \end{align*} Cutting $\Gamma \Rightarrow A \to B$ with this sequent gives $\Gamma \Rightarrow B$. For disjunction introduction, the induction hypothesis gives either $\Gamma \Rightarrow A$ or $\Gamma \Rightarrow B$, and the corresponding right rule gives $\Gamma \Rightarrow A \vee B$. For [disjunction elimination](/theorems/4625), suppose $\mathcal{D}$ derives $C$ from derivations of $\Gamma \vdash_{\mathrm{NJ}} A \vee B$, $\Gamma,A \vdash_{\mathrm{NJ}} C$, and $\Gamma,B \vdash_{\mathrm{NJ}} C$. By induction these become $\Gamma \Rightarrow A \vee B$, $\Gamma,A \Rightarrow C$, and $\Gamma,B \Rightarrow C$. The left rule for $\vee$ gives $\Gamma,A \vee B \Rightarrow C$, and cut with $\Gamma \Rightarrow A \vee B$ gives $\Gamma \Rightarrow C$. For falsity elimination, suppose the last rule derives $A$ from $\Gamma \vdash_{\mathrm{NJ}} \bot$. By induction, $\Gamma \Rightarrow \bot$ is derivable. The left rule for $\bot$ gives $\bot \Rightarrow A$, and cut gives $\Gamma \Rightarrow A$. These cases exhaust the standard rules of intuitionistic natural deduction, so every $\mathrm{NJ}$ derivation yields an $\mathrm{LJ}$ derivation of the corresponding sequent. [guided] The induction follows the shape of the natural-deduction proof tree. At each last rule, we assume that every immediate subderivation has already been translated into a sequent derivation with the same open assumptions and the same conclusion formula. The introduction rules are direct. If natural deduction introduces $A \wedge B$, then the two premises are derivations of $A$ and $B$ from the same assumptions, and the $\mathrm{LJ}$ right rule for $\wedge$ has exactly those premises: \begin{align*} \frac{\Gamma \Rightarrow A \qquad \Gamma \Rightarrow B}{\Gamma \Rightarrow A \wedge B}. \end{align*} The same pattern applies to $\vee$-introduction and $\to$-introduction: right rules in $\mathrm{LJ}$ record exactly what the introduction rules require. The elimination rules require one additional idea: the eliminated formula is first produced, then consumed. In sequent calculus, this two-stage process is represented by a left rule followed by cut. For example, from a derivation of $\Gamma \vdash_{\mathrm{NJ}} A \wedge B$, the induction hypothesis gives $\Gamma \Rightarrow A \wedge B$. The $\wedge$-left rule proves that an assumption $A \wedge B$ is enough to obtain $A$, because from the identity axiom $A \Rightarrow A$ we derive $A \wedge B \Rightarrow A$. Cutting the produced formula $A \wedge B$ against this use of $A \wedge B$ gives $\Gamma \Rightarrow A$. Modus ponens is the same phenomenon for implication. The induction hypothesis gives $\Gamma \Rightarrow A \to B$ and $\Gamma \Rightarrow A$. The $\to$-left rule expresses that, from an assumption $A \to B$, one may obtain $B$ once $A$ is available: \begin{align*} \frac{\Gamma \Rightarrow A \qquad B \Rightarrow B}{\Gamma,A \to B \Rightarrow B}. \end{align*} A final cut with $\Gamma \Rightarrow A \to B$ removes the temporary assumption $A \to B$ and yields $\Gamma \Rightarrow B$. Disjunction elimination is case analysis. The induction hypothesis gives derivations of $\Gamma,A \Rightarrow C$ and $\Gamma,B \Rightarrow C$, so the $\vee$-left rule says that $\Gamma,A \vee B \Rightarrow C$. Since the major premise gives $\Gamma \Rightarrow A \vee B$, cut yields $\Gamma \Rightarrow C$. Falsity elimination is handled by the $\bot$-left rule in the same way. Thus every natural-deduction rule has a sound sequent-calculus simulation. [/guided] [/step] [step:Translate $\mathrm{LJ}$ derivations into intuitionistic natural deduction derivations] We prove, by induction on an $\mathrm{LJ}$ derivation of $\Gamma \Rightarrow A$, that $\Gamma \vdash_{\mathrm{NJ}} A$. The identity axiom $A \Rightarrow A$ translates to the open assumption $A \vdash_{\mathrm{NJ}} A$. Weakening, exchange, and contraction translate to adding unused assumptions, reordering open assumptions, and reusing an assumption. The right rules translate into the corresponding introduction rules. Thus $\wedge_R$ translates to conjunction introduction, $\vee_R$ to the appropriate disjunction introduction, $\to_R$ to implication introduction by discharging the antecedent assumption, and the absence of a right rule for $\bot$ requires no separate case. The left rules translate into the corresponding elimination principles. For $\wedge_L$, a derivation of $\Gamma,A,B \vdash_{\mathrm{NJ}} C$ gives a derivation of $\Gamma,A \wedge B \vdash_{\mathrm{NJ}} C$ by applying conjunction eliminations to the open assumption $A \wedge B$ to obtain $A$ and $B$, then substituting those derivations into the derivation of $C$. For $\vee_L$, derivations of $\Gamma,A \vdash_{\mathrm{NJ}} C$ and $\Gamma,B \vdash_{\mathrm{NJ}} C$ give $\Gamma,A \vee B \vdash_{\mathrm{NJ}} C$ by disjunction elimination. For $\to_L$, derivations of $\Gamma \vdash_{\mathrm{NJ}} A$ and $\Gamma,B \vdash_{\mathrm{NJ}} C$ give $\Gamma,A \to B \vdash_{\mathrm{NJ}} C$ by first applying modus ponens to the assumptions $A \to B$ and the derivation of $A$, obtaining $B$, and then substituting that derivation of $B$ into the derivation of $C$. For $\bot_L$, the rule translates to falsity elimination. Finally, the cut rule translates to composition of natural-deduction derivations. If the premises translate to $\Gamma \vdash_{\mathrm{NJ}} A$ and $\Gamma,A \vdash_{\mathrm{NJ}} B$, then substituting the first derivation for every open occurrence of the assumption $A$ in the second gives $\Gamma \vdash_{\mathrm{NJ}} B$. Therefore every $\mathrm{LJ}$ derivation of $\Gamma \Rightarrow A$ yields an $\mathrm{NJ}$ derivation of $\Gamma \vdash_{\mathrm{NJ}} A$. [/step] [step:Encode finite classical succedents as single disjunctions] For every finite succedent $\Delta=(A_1,\dots,A_n)$, define $\bigvee\Delta$ as in the statement. The empty succedent is encoded by $\bot$, so a sequent $\Gamma \Rightarrow \varnothing$ is read as the classical natural-deduction assertion $\Gamma \vdash_{\mathrm{NK}} \bot$. If $E$ is a formula and a specified succedent position is fixed, write $D_{\Delta,E}$ for the finite disjunction obtained from the finite list formed by inserting $E$ into $\Delta$ at that position; in the append-at-the-end case this is $D_{\Delta,E}:=\bigvee(\Delta,E)$. Write $\iota_E:E\vdash_{\mathrm{NK}}D_{\Delta,E}$ for the natural-deduction derivation obtained by repeated $\vee$-introduction that places the open formula $E$ in that specified disjunct position. The structural rules on the succedent are respected by classical natural deduction. More explicitly, for any two finite lists $\Delta$ and $\Delta'$ containing the same formulas with the same multiplicities, a finite induction on adjacent transpositions gives derivations $\bigvee\Delta\vdash_{\mathrm{NK}}\bigvee\Delta'$ and $\bigvee\Delta'\vdash_{\mathrm{NK}}\bigvee\Delta$: each adjacent transposition is handled by one $\vee$-elimination on the two swapped alternatives and the two corresponding $\vee$-introductions into the target bracketing. Weakening from $\Delta$ to $(\Delta,E)$ is the repeated disjunction-introduction derivation inserting the already selected alternative into the larger disjunction. Contraction is handled by induction on the position of the repeated formula, reducing the principal case $A\vee A\vdash_{\mathrm{NK}}A$ by $\vee$-elimination with both branches the open assumption $A$, and carrying the contraction through surrounding disjunctions by $\vee$-elimination and reintroduction. In the empty-succedent case there is no disjunct to rearrange or contract. [/step] [step:Translate $\mathrm{LK}$ derivations into classical natural deduction] We prove, by induction on an $\mathrm{LK}$ derivation of $\Gamma \Rightarrow \Delta$, that $\Gamma \vdash_{\mathrm{NK}} \bigvee \Delta$. An initial axiom $\Gamma,A \Rightarrow \Delta,A$ translates to a derivation of $\bigvee(\Delta,A)$ from the open assumption $A$: derive $A$ by assumption and then introduce the disjunct corresponding to $A$. Structural rules translate as described above. For right rules, write $D_\Delta$ for $\bigvee\Delta$ and write $\iota_E:E\vdash_{\mathrm{NK}}D_{\Delta,E}$ for the repeated disjunction-introduction derivation placing the formula $E$ in its indicated succedent position. The $\vee_R$ case is obtained by finite disjunction elimination on the induction-hypothesis derivation of $D_{\Delta,A,B}$: every $E\in\Delta$-case is sent to $D_{\Delta,A\vee B}$ by $\iota_E$, the $A$-case is sent by first introducing $A\vee B$ and then applying $\iota_{A\vee B}$, and the $B$-case is handled analogously. For $\wedge_R$, the premises translate to derivations \begin{align*} \Gamma &\vdash_{\mathrm{NK}} D_{\Delta,A},\\ \Gamma &\vdash_{\mathrm{NK}} D_{\Delta,B}. \end{align*} We derive $D_{\Delta,A\wedge B}$ from the first derivation by finite disjunction elimination. If the selected case is some $E\in\Delta$, apply $\iota_E$. If the selected case is $A$, then eliminate the second derivation of $D_{\Delta,B}$: an $E\in\Delta$-case again gives $D_{\Delta,A\wedge B}$ by $\iota_E$, while the $B$-case combines the open assumptions $A$ and $B$ by conjunction introduction to obtain $A\wedge B$, then applies $\iota_{A\wedge B}$. This constructs a derivation of $\Gamma\vdash_{\mathrm{NK}}D_{\Delta,A\wedge B}$. For $\to_R$, the premise $\Gamma,A\Rightarrow\Delta,B$ translates to a derivation of $\Gamma,A\vdash_{\mathrm{NK}}D_{\Delta,B}$. Let $P$ denote the formula $D_{\Delta,A\to B}$. We use the classical natural-deduction rule of reductio: from a derivation of $\bot$ under a temporary assumption $P\to\bot$, infer $P$. Assume temporarily $P\to\bot$. Under a further temporary assumption $A$, the premise translation gives $D_{\Delta,B}$. Eliminate this finite disjunction. In an $E\in\Delta$-case, $\iota_E$ gives $P$, contradicting $P\to\bot$, and falsity elimination gives $B$. In the $B$-case, use the open assumption $B$. Thus, under the sole temporary assumption $P\to\bot$, we have derived $A\to B$ by discharging the temporary assumption $A$. Applying $\iota_{A\to B}$ gives $P$, and applying $P\to\bot$ gives $\bot$. Hence reductio gives $\Gamma\vdash_{\mathrm{NK}}D_{\Delta,A\to B}$. For left rules, the principal formula is an open assumption, but the ambient finite succedent must still be handled by cases. The $\wedge_L$ case replaces an open assumption $A\wedge B$ by the two assumptions obtained from conjunction elimination and then uses the translated premise. The $\vee_L$ case applies disjunction elimination to the open assumption $A\vee B$ and uses the two translated premises. The $\bot_L$ case applies falsity elimination to the open assumption $\bot$ to obtain $D_\Delta$. For $\to_L$, the premises are $\Gamma\Rightarrow\Delta,A$ and $\Gamma,B\Rightarrow\Delta$. Their translations are \begin{align*} \Gamma &\vdash_{\mathrm{NK}}D_{\Delta,A},\\ \Gamma,B &\vdash_{\mathrm{NK}}D_\Delta. \end{align*} Working under the open assumption $A\to B$, eliminate the first finite disjunction $D_{\Delta,A}$. In an $E\in\Delta$-case, introduce the corresponding disjunct of $D_\Delta$. In the $A$-case, apply modus ponens to $A\to B$ and $A$ to derive $B$, then substitute this derivation of $B$ into the second translated premise to obtain $D_\Delta$. Therefore $\Gamma,A\to B\vdash_{\mathrm{NK}}D_\Delta$, which is the translation of the $\to_L$ conclusion. For cut, suppose the premises are $\Gamma \Rightarrow \Delta,A$ and $\Gamma,A \Rightarrow \Delta$. By the induction hypothesis, \begin{align*} \Gamma &\vdash_{\mathrm{NK}} \bigvee(\Delta,A),\\ \Gamma,A &\vdash_{\mathrm{NK}} \bigvee\Delta. \end{align*} From the first derivation, reason by cases on $\bigvee(\Delta,A)$. In every disjunct belonging to $\Delta$, introduce the corresponding disjunct of $\bigvee\Delta$. In the $A$-case, use the second derivation to obtain $\bigvee\Delta$. Therefore $\Gamma \vdash_{\mathrm{NK}} \bigvee\Delta$, which is the translation of the cut conclusion. This completes the induction from $\mathrm{LK}$ to $\mathrm{NK}$. [guided] The key point is that a classical sequent with several formulas on the right is translated as one conclusion: the finite disjunction of all right-hand formulas. Write $D_\Delta$ for $\bigvee\Delta$. Thus $\Gamma\Rightarrow A_1,A_2,A_3$ becomes the natural-deduction assertion that $\Gamma$ derives $A_1\vee(A_2\vee A_3)$, with the chosen bracketing fixed once and for all. The induction on the $\mathrm{LK}$ derivation follows the last rule, but the ambient disjunction $D_\Delta$ must be carried through every case. Initial sequents are direct: if $A$ occurs on both sides, the open assumption $A$ gives that alternative, and repeated disjunction introduction places it in $D_{\Delta,A}$. Consider the nontrivial right rules. For $\vee_R$, a derivation of $D_{\Delta,A,B}$ is eliminated by cases. An old alternative $E\in\Delta$ is reintroduced into $D_{\Delta,A\vee B}$; the $A$-case first derives $A\vee B$ by left disjunction introduction; the $B$-case first derives $A\vee B$ by right disjunction introduction. For $\wedge_R$, the translated premises derive $D_{\Delta,A}$ and $D_{\Delta,B}$. Eliminate the first disjunction. Old $\Delta$-cases are reintroduced immediately. In the $A$-case, eliminate the second disjunction: old $\Delta$-cases are again reintroduced, while the $B$-case gives both $A$ and $B$, hence $A\wedge B$, which is then inserted as the selected alternative of $D_{\Delta,A\wedge B}$. The $\to_R$ rule is where classical reasoning is used explicitly. The premise translates to $\Gamma,A\vdash_{\mathrm{NK}}D_{\Delta,B}$, and the goal is $P:=D_{\Delta,A\to B}$. Use reductio ad absurdum, the classical natural-deduction rule that permits deriving $P$ from a derivation of $\bot$ under a temporary assumption $P\to\bot$. Assume $P\to\bot$. Our task under this assumption is to derive $\bot$ without leaving any extra temporary assumption open. To do that, first derive $A\to B$. Assume $A$ temporarily. The translated premise gives $D_{\Delta,B}$. Eliminate this finite disjunction. In an old $E\in\Delta$-case, introduce $E$ into $P$, apply $P\to\bot$ to obtain $\bot$, and then use falsity elimination to obtain $B$. In the $B$-case, the branch already has $B$. Therefore the disjunction elimination gives $B$ under the temporary assumption $A$, and discharging $A$ gives $A\to B$ under the sole remaining temporary assumption $P\to\bot$. Now introduce $A\to B$ into the selected disjunct of $P$. Applying $P\to\bot$ gives $\bot$. Thus $P\to\bot$ yields $\bot$, so reductio gives $P$. Left rules consume assumptions while preserving the translated succedent. For $A\wedge B$ on the left, project $A$ and $B$ from the open assumption and use the translated premise. For $A\vee B$ on the left, apply disjunction elimination to the open assumption and use the translated premises in the two branches. For $A\to B$ on the left, the first premise gives $D_{\Delta,A}$ and the second gives $D_\Delta$ from an additional assumption $B$. Eliminate $D_{\Delta,A}$: old $\Delta$-cases are reintroduced into $D_\Delta$, and the $A$-case gives $B$ by modus ponens from the open assumption $A\to B$, after which the second premise yields $D_\Delta$. Cut is composition through an intermediate alternative. If we know $\Gamma\vdash_{\mathrm{NK}}D_{\Delta,A}$ and $\Gamma,A\vdash_{\mathrm{NK}}D_\Delta$, eliminate $D_{\Delta,A}$. The cases already belonging to $\Delta$ are reintroduced into $D_\Delta$; the $A$-case uses the second derivation. This exactly matches the $\mathrm{LK}$ cut rule. [/guided] [/step] [step:Translate classical natural deduction into $\mathrm{LK}$] We first prove the stronger statement: for every formula $C$, if $\Gamma\vdash_{\mathrm{NK}}C$, then the single-succedent sequent $\Gamma\Rightarrow C$ is derivable in $\mathrm{LK}$. The proof is by induction on the given $\mathrm{NK}$ derivation of $C$. Assumptions translate to identity axioms followed by weakening and exchange; the intuitionistic introduction and elimination rules translate exactly as in the $\mathrm{NJ}$ to $\mathrm{LJ}$ direction, using the corresponding $\mathrm{LK}$ rules and cut. We take the classical natural-deduction presentation to be intuitionistic natural deduction plus the excluded-middle rule schema deriving $C\vee(C\to\bot)$ for every formula $C$. This schema is derivable in $\mathrm{LK}$ as follows. From the identity axiom $C\Rightarrow C$, right weakening gives $C\Rightarrow C,\bot$. Applying $\to_R$ to the temporary antecedent $C$ gives $\Rightarrow C,C\to\bot$. Applying $\vee_R$ gives $\Rightarrow C\vee(C\to\bot)$. Any presentation using reductio or double-negation elimination may be expanded into this excluded-middle presentation, since these principles are interderivable in classical natural deduction. Now let the conclusion formula be $D_\Delta:=\bigvee\Delta$. The stronger induction gives an $\mathrm{LK}$ derivation of $\Gamma\Rightarrow D_\Delta$. It remains to decode the finite disjunction into the finite succedent. We prove by induction on the length of $\Delta$ that $D_\Delta\Rightarrow\Delta$ is derivable. If $\Delta=\varnothing$, then $D_\Delta=\bot$, and $\bot_L$ gives $\bot\Rightarrow\varnothing$. If $\Delta=(A,\Delta')$, then $D_\Delta=A\vee D_{\Delta'}$. The left branch $A\Rightarrow A,\Delta'$ follows from identity and right weakening. The right branch $D_{\Delta'}\Rightarrow A,\Delta'$ follows from the induction hypothesis $D_{\Delta'}\Rightarrow\Delta'$ by right weakening. Applying $\vee_L$ gives $A\vee D_{\Delta'}\Rightarrow A,\Delta'$, namely $D_\Delta\Rightarrow\Delta$. Cutting $\Gamma\Rightarrow D_\Delta$ with $D_\Delta\Rightarrow\Delta$ yields $\Gamma\Rightarrow\Delta$. In the empty-succedent case this cut is precisely the passage from $\Gamma\Rightarrow\bot$ and $\bot\Rightarrow\varnothing$ to $\Gamma\Rightarrow\varnothing$. Thus every classical natural-deduction derivation of $\Gamma\vdash_{\mathrm{NK}}\bigvee\Delta$ yields an $\mathrm{LK}$ derivation of $\Gamma\Rightarrow\Delta$. [/step] [step:Combine the four translations] The second and third steps prove \begin{align*} \Gamma \vdash_{\mathrm{NJ}} A \quad \Longleftrightarrow \quad \Gamma \Rightarrow A \text{ is derivable in } \mathrm{LJ}. \end{align*} The fourth and fifth steps prove \begin{align*} \Gamma \Rightarrow \Delta \text{ is derivable in } \mathrm{LK} \quad \Longleftrightarrow \quad \Gamma \vdash_{\mathrm{NK}} \bigvee\Delta. \end{align*} These are exactly the intuitionistic and classical assertions in the theorem, so the proof is complete. [/step]