[proofplan] We work with the standard ordered-context presentations of $LJ$ and $LK$ whose identity axioms are contextual identity axioms. The admissible weakening operations considered are exactly those that preserve the sequent shape of the calculus: antecedent weakening in $LJ$, and antecedent or succedent weakening in $LK$; there is no $LJ$ weakening from an empty succedent to a singleton succedent. The proof is by [induction on derivation height](/theorems/4623): weakening and exchange are pushed upward through the last logical inference and then the same inference is re-applied. The contextual identity axioms provide the base case because inserting or reordering side formulas preserves the distinguished identical formula occurrence. [/proofplan] [step:Fix the context notation, rule presentation, and induction parameter] A context is a finite ordered list of formulas. We write $\Gamma,\Pi$ for concatenation of contexts, and we write $\Gamma,A,\Pi$ for the context obtained by inserting the formula $A$ between $\Gamma$ and $\Pi$. In $LK$, both antecedent and succedent contexts are finite ordered lists. In $LJ$, antecedent contexts are finite ordered lists and succedent contexts have length at most one. We use the standard ordered-context propositional rules for $\wedge,\vee,\to,\neg$ in which each rule displays its principal formula and carries arbitrary ordered side contexts unchanged from premise to conclusion. More precisely, each rule instance is obtained from a fixed local pattern by inserting arbitrary ordered contexts around the displayed principal and auxiliary formulas. Thus a one-premise left rule has the form \begin{align*} \frac{\Gamma,\Sigma_1,\Pi \Rightarrow \Delta}{\Gamma,\Sigma_0,\Pi \Rightarrow \Delta}, \end{align*} where $\Sigma_0$ is the list consisting of the principal formula and $\Sigma_1$ is the list of auxiliary formulas required by that rule. A two-premise left rule has the form \begin{align*} \frac{\Gamma,\Sigma_1,\Pi \Rightarrow \Delta \qquad \Gamma,\Sigma_2,\Pi \Rightarrow \Delta}{\Gamma,\Sigma_0,\Pi \Rightarrow \Delta}. \end{align*} Right rules have the analogous form on the succedent side in $LK$; in $LJ$ the right rules are the usual single-succedent instances, with the side condition that each premise and conclusion has at most one succedent formula. For example, the ordered-context implication-left rule has the form \begin{align*} \frac{\Gamma,\Pi \Rightarrow \Delta,A \qquad \Gamma,B,\Pi \Rightarrow \Delta}{\Gamma,A\to B,\Pi \Rightarrow \Delta} \end{align*} in $LK$, with the corresponding single-succedent restriction in $LJ$ where applicable. The identity axioms are contextual: in $LK$ they have the form $\Gamma,A,\Pi \Rightarrow \Delta,A,\Theta$, and in $LJ$ they have the form $\Gamma,A,\Pi \Rightarrow A$. Here $A$ is the distinguished identity formula, while $\Gamma,\Pi,\Delta,\Theta$ are arbitrary contexts allowed by the calculus. For this proof, an allowed weakening operation means insertion of one formula into the antecedent context in $LJ$, insertion of one formula into either context in $LK$, and no operation inserting a new formula into an empty $LJ$ succedent. An allowed exchange operation means a finite permutation of the antecedent context in $LJ$, a finite permutation of either context in $LK$, and only the identity permutation on the $LJ$ succedent. For a derivation $\mathcal{D}$, let $h(\mathcal{D}) \in \mathbb{N} \cup \{0\}$ denote its height, meaning the maximum number of inference-rule applications on a branch from an initial sequent to the conclusion. We prove, simultaneously by induction on $h(\mathcal{D})$, the following two assertions. First, if $\mathcal{D}$ derives $\Gamma \Rightarrow \Delta$, then every sequent obtained by applying one allowed weakening operation to $\Gamma \Rightarrow \Delta$ is derivable. Second, if $\mathcal{D}$ derives $\Gamma \Rightarrow \Delta$, then every sequent obtained by applying one allowed exchange operation to $\Gamma \Rightarrow \Delta$ is derivable. [/step] [step:Verify weakening and exchange for initial sequents] Suppose $h(\mathcal{D})=0$. Then the conclusion of $\mathcal{D}$ is a contextual identity axiom. In $LK$ it has the form \begin{align*} \Gamma,A,\Pi \Rightarrow \Delta,A,\Theta, \end{align*} and in $LJ$ it has the form \begin{align*} \Gamma,A,\Pi \Rightarrow A. \end{align*} Here $A$ is the distinguished identity formula, and the other displayed contexts are arbitrary contexts allowed by the calculus. After inserting an additional formula into an allowed antecedent context, and also into an allowed succedent context in $LK$, the distinguished occurrence of $A$ on the left and the distinguished occurrence of $A$ on the right are still present. The resulting sequent is therefore again an instance of the same contextual identity axiom schema. No $LJ$ case inserts a formula into an empty succedent, because that operation is not an allowed weakening operation in the statement being proved. After permuting the formulas in the antecedent and, in $LK$, the succedent, the same formula $A$ still occurs on both sides. Choosing those occurrences as the distinguished identity pair makes the permuted sequent an instance of the contextual identity axiom schema. This proves both admissibility assertions for derivations of height zero. [guided] At height zero there is no last logical rule to analyze. The derivation is just an initial sequent, and in the presentation fixed above initial sequents are contextual identity axioms. Thus an initial sequent in $LK$ has the form \begin{align*} \Gamma,A,\Pi \Rightarrow \Delta,A,\Theta, \end{align*} and an initial sequent in $LJ$ has the form \begin{align*} \Gamma,A,\Pi \Rightarrow A. \end{align*} The formula $A$ is the distinguished identity formula. The contexts $\Gamma,\Pi,\Delta,\Theta$ are arbitrary ordered contexts of the kind allowed in the corresponding calculus. Consider weakening first. If we insert a new formula into the antecedent of either calculus, or into the succedent of $LK$, the two distinguished occurrences of $A$ remain in the sequent. Therefore the weakened sequent is still an instance of the contextual identity axiom schema. There is no case in which we insert a formula into an empty $LJ$ succedent, because that operation would not preserve the sequent shape covered by the theorem. Now consider exchange. A finite permutation of the antecedent in $LJ$, or of either side in $LK$, merely changes the order of the surrounding context formulas. The two occurrences of $A$ remain available as the matching identity pair. Hence the permuted sequent is again an instance of the contextual identity axiom schema. This proves the base case for both transformations. [/guided] [/step] [step:Propagate an inserted formula through the last inference] Assume the weakening assertion has been proved for all derivations of height less than $h$, and let $\mathcal{D}$ be a derivation of height $h>0$ with conclusion $\Gamma \Rightarrow \Delta$. Let $R$ be the last inference rule of $\mathcal{D}$. If the inserted formula is placed in a side context of the conclusion of $R$, insert the same formula in the corresponding side context of every premise of $R$. Each premise has a derivation of height less than $h$, so the induction hypothesis gives derivations of the weakened premises. Re-applying $R$ to these weakened premises gives the desired weakened conclusion. It remains to note that this covers every propositional rule of $LJ$ and $LK$. The left rules for $\wedge,\vee,\to,\neg$ and the right rules for $\wedge,\vee,\to,\neg$ are all schematic in their side contexts: adding a formula to a side context does not change the principal formula and does not change the auxiliary formulas required by the rule. For a binary rule, such as $\wedge R$ in $LJ$ or $\to L$ in either calculus, the same inserted formula is added to each premise context to which the conclusion context corresponds. For a unary rule, it is added to the unique corresponding premise context. The re-applied inference is therefore an instance of the same rule $R$. If the inserted formula is placed immediately next to a principal formula in the conclusion, we still regard it as part of the adjacent side context. The principal occurrence itself is unchanged, so the same last rule applies after weakening the premises. Thus weakening is admissible for derivations of height $h$. [guided] Suppose the final line of the derivation is obtained by a logical rule $R$, and let $E$ be the formula inserted by weakening. In the ordered-context schema fixed above, each premise context is obtained from the conclusion context by replacing the principal formula list $\Sigma_0$ by one of the auxiliary formula lists $\Sigma_i$, while leaving the surrounding contexts $\Gamma$ and $\Pi$ unchanged. Therefore an insertion of $E$ into a side context of the conclusion determines the same insertion of $E$ into the corresponding side context of every premise. For example, if the last rule is a right conjunction rule in $LJ$, \begin{align*} \frac{\Gamma \Rightarrow A \qquad \Gamma \Rightarrow B}{\Gamma \Rightarrow A \wedge B}, \end{align*} then antecedent weakening at the end asks for a derivation of $\Gamma,E \Rightarrow A\wedge B$. The two premise derivations have smaller height, so the induction hypothesis gives derivations of \begin{align*} \Gamma,E \Rightarrow A \qquad\text{and}\qquad \Gamma,E \Rightarrow B. \end{align*} Applying the same right conjunction rule gives \begin{align*} \Gamma,E \Rightarrow A \wedge B. \end{align*} The generic ordered-context schema gives the identical construction for every unary and binary rule. A unary rule requires weakening its unique premise. A binary rule requires weakening both premises in the side context inherited by the conclusion. In $LK$, the same argument applies on the succedent side because right and left rules carry arbitrary ordered succedent side contexts unchanged. In $LJ$, the side condition is preserved because the allowed weakening operations insert only into the antecedent; no operation creates a new formula in an empty succedent. If $E$ is placed immediately next to the principal formula in the conclusion, we treat $E$ as part of the adjacent side context rather than as part of the principal formula list $\Sigma_0$. The principal occurrence remains the same occurrence, and the auxiliary formula lists in the premises are unchanged. Hence the final inference after weakening is still an instance of the same rule $R$. Since every premise derivation has height less than $h$, the induction hypothesis supplies all weakened premises. Re-applying the last rule completes the induction step for weakening. [/guided] [/step] [step:Push a context permutation through the last inference] Assume the exchange assertion has been proved for all derivations of height less than $h$, and let $\mathcal{D}$ be a derivation of height $h>0$ with conclusion $\Gamma \Rightarrow \Delta$. Let $R$ be the last inference rule. Let $\sigma$ be a permutation of an allowed context in the conclusion. We must derive the sequent obtained by applying $\sigma$. If $\sigma$ only permutes side-context formulas of $R$, apply the corresponding permutation to the matching side contexts in every premise. The induction hypothesis gives derivations of the permuted premises, and the same rule $R$ gives the permuted conclusion. Now suppose the permutation moves a principal formula of $R$ past neighboring context formulas. It is enough to check an adjacent exchange, because finite permutations are products of adjacent exchanges. Write the conclusion-side context around the principal formula as $\Gamma,E,\Sigma_0,\Pi$ or $\Gamma,\Sigma_0,E,\Pi$, where $E$ is the neighboring side formula and $\Sigma_0$ is the displayed principal formula list of $R$. In every premise of $R$, replace this local segment by $\Gamma,E,\Sigma_i,\Pi$ or $\Gamma,\Sigma_i,E,\Pi$, where $\Sigma_i$ is the corresponding auxiliary formula list for that premise. The induction hypothesis gives these premise permutations because each premise derivation has smaller height. This local description checks the nonuniform binary rules. For disjunction-left, the two premise lists are $\Sigma_1=(A)$ and $\Sigma_2=(B)$ while the conclusion list is $\Sigma_0=(A\vee B)$; exchanging $E$ across $A\vee B$ in the conclusion is obtained by exchanging $E$ across $A$ in the first premise and across $B$ in the second premise. For implication-left, the premise lists are empty on the premise whose succedent contains $A$ and $(B)$ on the premise whose antecedent contains $B$, while the conclusion list is $(A\to B)$; exchanging $E$ across $A\to B$ in the conclusion is obtained by exchanging $E$ across the empty local list in the first premise, which only moves $E$ inside the inherited side context, and across $B$ in the second premise. The negation-left and negation-right rules are the same unary instance of this replacement rule, with the auxiliary formula occurring on the opposite side when required by the calculus. After these premise permutations, re-apply $R$ with the principal occurrence in its new position. The conclusion is exactly the desired adjacent exchange of $\Gamma \Rightarrow \Delta$. Since every finite permutation is a finite product of adjacent exchanges, exchange is admissible for arbitrary finite permutations of antecedent contexts and, in $LK$, succedent contexts. In $LJ$, the succedent has length at most one, so there is no nontrivial succedent exchange. [guided] It is enough to prove admissibility for an adjacent interchange, because every finite permutation of a finite ordered list is a finite composition of adjacent interchanges. Let the desired adjacent interchange occur in the conclusion of the last rule $R$. If the two exchanged formulas are both side formulas for $R$, the displayed principal and auxiliary formulas of $R$ are unchanged. We apply the induction hypothesis to perform the same adjacent interchange in each premise context inherited from the conclusion, then re-apply $R$. Now suppose one exchanged formula is principal. Write the local conclusion context as $\Gamma,E,\Sigma_0,\Pi$ or $\Gamma,\Sigma_0,E,\Pi$, where $E$ is the neighboring side formula and $\Sigma_0$ is the principal formula list of the rule. In the $i$th premise, the same rule has the corresponding local list $\Sigma_i$ of auxiliary formulas. We use the induction hypothesis to replace the premise context by $\Gamma,E,\Sigma_i,\Pi$ or $\Gamma,\Sigma_i,E,\Pi$, matching the desired side of the exchange. This is a legitimate use of the induction hypothesis because the premise derivations have height less than $h$. This construction also covers rules whose premises have different auxiliary formulas. For disjunction-left, the conclusion list is $\Sigma_0=(A\vee B)$, while the two premise lists are $\Sigma_1=(A)$ and $\Sigma_2=(B)$. Moving $E$ past $A\vee B$ in the conclusion is therefore obtained by moving $E$ past $A$ in the first premise and past $B$ in the second premise. For implication-left, the conclusion list is $\Sigma_0=(A\to B)$; the premise in which $A$ occurs on the succedent side has no antecedent auxiliary formula at that local position, while the other premise has antecedent list $\Sigma_i=(B)$. Thus the required premise permutations move $E$ in the inherited side context of the first premise and move $E$ past $B$ in the second premise. The same local-list argument applies to the unary negation rules and to the right rules, with the local list placed on the succedent side in $LK$ and subject to the single-succedent restriction in $LJ$. After these premise permutations, we re-apply $R$ and choose the displayed occurrence of $\Sigma_0$ in its new location as the principal occurrence. The resulting conclusion is precisely the adjacent exchange desired at height $h$. Repeating adjacent exchanges gives any finite permutation. In $LK$ this applies on both sides of the sequent. In $LJ$ it applies on the antecedent side, while the succedent side has at most one formula and therefore admits no nontrivial exchange. [/guided] [/step] [step:Conclude admissibility for the structural rules] The induction on derivation height proves that every allowed weakening instance whose conclusion respects the side conditions fixed above transforms derivable premises into a derivable conclusion. Hence antecedent weakening is admissible in $LJ$, and antecedent and succedent weakening are admissible in $LK$. The same induction proves that every adjacent exchange in an allowed context transforms derivable sequents into derivable sequents, and finite compositions of adjacent exchanges give all finite permutations. Hence antecedent exchange is admissible in $LJ$, and antecedent and succedent exchange are admissible in $LK$. Therefore, in the standard ordered-context propositional sequent calculi $LJ$ and $LK$ with the contextual identity presentation and schematic side-context rules fixed above, these weakening and exchange rules are admissible whenever they are omitted as primitive rules. [/step]