[proofplan] We prove the stronger admissibility theorem: if the two premises of a cut are already cut-free derivable, then its conclusion is cut-free derivable. The proof is by lexicographic induction on the complexity of the cut formula and then on the sum of the heights of the two cut-free derivations. Principal-principal cuts are replaced by cuts on proper subformulas, while every non-principal cut is permuted above the last inference of the premise in which the cut formula is not principal. Once cut admissibility is established, a final induction on the given derivation eliminates every occurrence of the cut rule from the bottom upward. [/proofplan] [step:Define the induction measure for a single cut] For a propositional formula $C$, define its complexity $|C| \in \mathbb{N}$ recursively by setting $|P| = 0$ for an atomic proposition $P$, $|\bot| = 0$, and \begin{align*} |A \land B| &= 1 + |A| + |B|, \\ |A \lor B| &= 1 + |A| + |B|, \\ |A \to B| &= 1 + |A| + |B|. \end{align*} For a cut-free derivation $\mathcal{D}$, let $h(\mathcal{D}) \in \mathbb{N}$ denote its height. We prove the following admissibility statement by lexicographic induction on \begin{align*} \mu(C,\mathcal{D}_1,\mathcal{D}_2) = \bigl(|C|,\ h(\mathcal{D}_1)+h(\mathcal{D}_2)\bigr). \end{align*} If $\mathcal{D}_1$ is a cut-free derivation of $\Gamma \vdash C$ and $\mathcal{D}_2$ is a cut-free derivation of $\Delta, C, \Pi \vdash A$, then there exists a cut-free derivation of $\Delta, \Gamma, \Pi \vdash A$. The structural rules exchange, weakening, and contraction are available in the cut-free system, so throughout the proof we freely restore the displayed order and multiplicity of contexts by applying these structural rules explicitly when needed. [/step] [step:Handle cuts where the cut formula is introduced in both premises] Assume first that the last inference of $\mathcal{D}_1$ introduces the cut formula $C$ on the right and the last inference of $\mathcal{D}_2$ introduces that same occurrence of $C$ on the left. We replace the cut on $C$ by one or more cuts on proper subformulas of $C$. If $C = B \land D$, then $\mathcal{D}_1$ ends with $\land R$: \begin{align*} \frac{\Gamma \vdash B \qquad \Gamma \vdash D}{\Gamma \vdash B \land D}. \end{align*} The left introduction in $\mathcal{D}_2$ is either \begin{align*} \frac{\Delta, B, \Pi \vdash A}{\Delta, B \land D, \Pi \vdash A} \end{align*} or \begin{align*} \frac{\Delta, D, \Pi \vdash A}{\Delta, B \land D, \Pi \vdash A}. \end{align*} In the first case, the induction hypothesis applied to the proper subformula $B$ gives a cut-free derivation of $\Delta, \Gamma, \Pi \vdash A$. In the second case, the induction hypothesis applied to the proper subformula $D$ gives the same conclusion. If $C = B \lor D$, then $\mathcal{D}_1$ ends with either $\lor R_1$ or $\lor R_2$. In the first case it has premise $\Gamma \vdash B$, and $\mathcal{D}_2$ has the form \begin{align*} \frac{\Delta, B, \Pi \vdash A \qquad \Delta, D, \Pi \vdash A}{\Delta, B \lor D, \Pi \vdash A}. \end{align*} Applying the induction hypothesis to the cut formula $B$ and to the derivations of $\Gamma \vdash B$ and $\Delta, B, \Pi \vdash A$ gives a cut-free derivation of $\Delta, \Gamma, \Pi \vdash A$. The case where $\mathcal{D}_1$ ends with $\lor R_2$ is identical with $D$ in place of $B$. If $C = B \to D$, then $\mathcal{D}_1$ ends with $\to R$ and has a cut-free premise \begin{align*} \mathcal{E}_1:\Gamma, B \vdash D. \end{align*} The derivation $\mathcal{D}_2$ ends with $\to L$ and has cut-free premises \begin{align*} \mathcal{E}_2&:\Sigma \vdash B, \\ \mathcal{E}_3&:\Delta, D, \Pi \vdash A, \end{align*} with conclusion $\Delta, \Sigma, B \to D, \Pi \vdash A$, up to exchange. First apply the induction hypothesis to the cut formula $B$ using $\mathcal{E}_2$ and $\mathcal{E}_1$; since $|B| < |B \to D|$, this gives a cut-free derivation \begin{align*} \mathcal{F}_1:\Gamma, \Sigma \vdash D. \end{align*} Then apply the induction hypothesis to the cut formula $D$ using $\mathcal{F}_1$ and $\mathcal{E}_3$; since $|D| < |B \to D|$, this gives a cut-free derivation of $\Delta, \Gamma, \Sigma, \Pi \vdash A$. Exchange restores the required order of the context. There is no principal-principal case for $C = \bot$, since $\bot$ has no right introduction rule in $\mathsf{LJ}_{\mathrm{prop}}$. [/step] [step:Move the cut above a non-principal inference in the left premise] Assume the last inference of $\mathcal{D}_1$ does not introduce the cut formula $C$ as its principal formula. We permute the cut above that last inference. For a unary last inference, write its premise as a cut-free derivation \begin{align*} \mathcal{E}_1:\Gamma_0 \vdash E \end{align*} and its conclusion as $\Gamma \vdash C$. Since $C$ is not principal in this inference, the same inference may be applied after replacing the displayed premise derivation by the result of cutting its conclusion with $\mathcal{D}_2$. The premise cut has the same cut formula $C$, and the height of the left derivation has decreased from $h(\mathcal{D}_1)$ to $h(\mathcal{E}_1)$; hence the second coordinate of $\mu$ decreases. The induction hypothesis therefore gives the needed cut-free premise, and reapplying the same logical or structural inference gives a cut-free derivation of $\Delta,\Gamma,\Pi \vdash A$. For a binary last inference, let its cut-free premises be \begin{align*} \mathcal{E}_1:\Gamma_1 \vdash E_1, \qquad \mathcal{E}_2:\Gamma_2 \vdash E_2. \end{align*} Because $C$ is not principal, the occurrence of $C$ in the conclusion is inherited from one or both premises as a side formula. Apply the induction hypothesis to each premise containing that occurrence of $C$; in each such application the cut formula is still $C$, while the relevant premise height is strictly smaller than $h(\mathcal{D}_1)$. Reapply the same binary inference to the resulting cut-free premises. The conclusion is $\Delta,\Gamma,\Pi \vdash A$, up to exchange and contraction, and hence is cut-free derivable. This covers right rules whose principal formula is not $C$, left logical rules applied to formulas in the left context other than the displayed occurrence of $C$, and the structural rules applied away from the displayed occurrence of $C$. [/step] [step:Move the cut above a non-principal inference in the right premise] Assume now that the last inference of $\mathcal{D}_2$ does not introduce the displayed occurrence of $C$ as its principal formula. We permute the cut above that last inference in $\mathcal{D}_2$. If the last inference of $\mathcal{D}_2$ is unary, let its cut-free premise be $\mathcal{E}_2$. The displayed occurrence of $C$ is present in the premise as a side formula. The cut between $\mathcal{D}_1$ and $\mathcal{E}_2$ has the same cut formula $C$, the same left derivation $\mathcal{D}_1$, and a strictly smaller right height than $h(\mathcal{D}_2)$. By the induction hypothesis, its conclusion has a cut-free derivation. Reapplying the final unary inference gives the desired cut-free derivation of $\Delta,\Gamma,\Pi \vdash A$. If the last inference of $\mathcal{D}_2$ is binary, apply the induction hypothesis separately to each premise in which the displayed occurrence of $C$ appears. The cut formula remains $C$, but the right derivation height is smaller in each application. Reapplying the same binary inference gives the cut-free conclusion. The only structural point requiring mention is contraction on the displayed cut formula. In that case $\mathcal{D}_2$ has a premise of the form \begin{align*} \Delta, C, C, \Pi \vdash A \end{align*} and conclusion $\Delta, C, \Pi \vdash A$. First apply the induction hypothesis to $\mathcal{D}_1$ and the premise, cutting one displayed occurrence of $C$, to obtain a cut-free derivation of \begin{align*} \Delta, \Gamma, C, \Pi \vdash A. \end{align*} Apply the induction hypothesis again to the same left derivation $\mathcal{D}_1$ and this new derivation, cutting the remaining displayed occurrence of $C$, to obtain \begin{align*} \Delta, \Gamma, \Gamma, \Pi \vdash A. \end{align*} Finally apply contraction repeatedly to the formulas of the duplicated context $\Gamma$, together with exchange as needed, to obtain $\Delta,\Gamma,\Pi \vdash A$. [/step] [step:Close the admissibility induction] The cases above exhaust the possible last inferences of the two cut-free derivations. If the cut formula is principal in both premises, the first component of the induction measure decreases because every new cut formula is a proper subformula of $C$. If the cut formula is not principal in at least one premise, the cut is permuted above the corresponding last inference, so the first component is unchanged and the sum of derivation heights strictly decreases. Since lexicographic order on $\mathbb{N} \times \mathbb{N}$ is well-founded, the admissibility statement holds for every formula $C$ and every pair of cut-free derivations of the two cut premises. [/step] [step:Eliminate every cut from an arbitrary derivation] Let $\mathcal{D}$ be a derivation of $\Gamma \vdash A$ in $\mathsf{LJ}_{\mathrm{prop}}^{\mathrm{cut}}$. We prove by induction on $h(\mathcal{D})$ that $\Gamma \vdash A$ has a cut-free derivation. If $\mathcal{D}$ is an initial derivation, then it is already cut-free. If the last inference of $\mathcal{D}$ is a logical or structural rule, apply the induction hypothesis to each premise derivation and then reapply the same cut-free rule. It remains to consider the case where the last inference is cut: \begin{align*} \frac{\Gamma \vdash C \qquad \Delta, C, \Pi \vdash A}{\Delta,\Gamma,\Pi \vdash A}. \end{align*} By the induction hypothesis, both premises have cut-free derivations. Applying the cut-admissibility result proved above to these two cut-free premise derivations yields a cut-free derivation of $\Delta,\Gamma,\Pi \vdash A$. Therefore the conclusion of every derivation in $\mathsf{LJ}_{\mathrm{prop}}^{\mathrm{cut}}$ is derivable in the cut-free subsystem $\mathsf{LJ}_{\mathrm{prop}}$. [/step]