## Formalized Name Admissibility of Structural Rules in Schematic List-Context LJ ## Formalized Statement Let $\mathcal{L}$ be a first-order language, and let $\mathrm{LJ}^{-}_{\mathrm{list}}(\mathcal{L})$ denote the single-conclusion sequent calculus whose sequents have the form $\Gamma \Rightarrow S$, where $\Gamma$ is a finite list of $\mathcal{L}$-formulas and $S$ is either empty or one $\mathcal{L}$-formula. Assume that identity is the contextual initial rule $\Gamma,A,\Delta \Rightarrow A$, that the primitive logical rules are the usual intuitionistic left and right rules for $\top$, $\bot$, $\land$, $\lor$, $\to$, $\forall$, and $\exists$ with explicit finite list side contexts, and that left weakening, left exchange, and left contraction are not primitive inference rules. Assume also that these logical rule schemata are stable under uniform list-context reindexing: if one inserts the same extra formula occurrence into every antecedent list in a rule instance, swaps the same adjacent antecedent occurrences in every antecedent list in a rule instance, or identifies the same two adjacent equal formula occurrences in every antecedent list in a rule instance, the result is again an allowed instance of the same logical rule whenever the principal formulas and eigenvariable side conditions are unchanged. Then the following left structural rules are admissible in $\mathrm{LJ}^{-}_{\mathrm{list}}(\mathcal{L})$: insertion of an extra antecedent formula, swapping two adjacent antecedent formulas, and deleting one copy from two adjacent equal antecedent formulas. ## Proof [proofplan] The proof constructs derivation transformers rather than adding structural rules to the calculus. Contextual identity handles the initial sequents, and the uniform reindexing hypothesis lets the same context operation be pushed through every logical inference. Applying this recursion to insertion, adjacent exchange, and adjacent contraction gives derivations of exactly the desired conclusions from derivations of the corresponding premises. [/proofplan] [step:Define the three context operations on derivation trees] Let $\mathcal{D}$ denote a derivation tree in $\mathrm{LJ}^{-}_{\mathrm{list}}(\mathcal{L})$, and let $h(\mathcal{D}) \in \mathbb{N}$ denote its height. A context operation will mean one of the following three operations applied to every antecedent list in a derivation tree. For insertion, fix finite lists $\Gamma$ and $\Delta$ of $\mathcal{L}$-formulas and fix an $\mathcal{L}$-formula $B$. The insertion operation sends the sequent $\Gamma,\Delta \Rightarrow S$ to the sequent $\Gamma,B,\Delta \Rightarrow S$. For adjacent exchange, fix finite lists $\Gamma$ and $\Delta$ of $\mathcal{L}$-formulas and fix $\mathcal{L}$-formulas $A$ and $B$. The exchange operation sends the sequent $\Gamma,A,B,\Delta \Rightarrow S$ to the sequent $\Gamma,B,A,\Delta \Rightarrow S$. For adjacent contraction, fix finite lists $\Gamma$ and $\Delta$ of $\mathcal{L}$-formulas and fix an $\mathcal{L}$-formula $A$. The contraction operation sends the sequent $\Gamma,A,A,\Delta \Rightarrow S$ to the sequent $\Gamma,A,\Delta \Rightarrow S$. In each case the succedent $S$ is either empty or a single formula. The target is to show that, whenever the source sequent of the operation is derivable, the target sequent is derivable. [/step] [step:Transform contextual identity leaves] Consider a leaf of a derivation tree. Since the only nonlogical leaf rule used here is contextual identity, the leaf has the form $\Pi,C,\Lambda \Rightarrow C$ for finite lists $\Pi$ and $\Lambda$ and a formula $C$. After insertion, the transformed leaf still has $C$ in its antecedent list and still has succedent $C$. Hence it is again an instance of contextual identity. After adjacent exchange, the transformed leaf has the same formulas as the original antecedent list, only with two adjacent occurrences interchanged. Since the original antecedent list contained the displayed occurrence of $C$, the transformed antecedent list still contains an occurrence of $C$. Hence the transformed sequent is again an instance of contextual identity. After adjacent contraction, the transformed leaf is obtained by deleting one of two adjacent equal antecedent formulas. If the deleted occurrence is not the displayed identity occurrence $C$, then the displayed occurrence of $C$ remains. If the deleted occurrence is the displayed identity occurrence, then the retained adjacent equal occurrence is also $C$. In both cases the transformed leaf is again an instance of contextual identity. [guided] The base case is where the contextual form of identity is essential. A leaf has the form $\Pi,C,\Lambda \Rightarrow C$, where $\Pi$ and $\Lambda$ are finite lists and $C$ is a formula. The rule allows any surrounding antecedent list, provided that some displayed occurrence of $C$ remains on the left. After insertion, the antecedent list has one more formula occurrence, but the occurrence of $C$ from $\Pi,C,\Lambda \Rightarrow C$ is still present. Therefore the transformed sequent is another contextual identity sequent. After adjacent exchange, two neighboring antecedent occurrences have changed order. The antecedent list still contains an occurrence of $C$, so the transformed sequent is again an allowed identity leaf with succedent $C$. After adjacent contraction, one of two adjacent equal formula occurrences is deleted. If the deleted occurrence is not the occurrence of $C$ used by identity, then that same occurrence of $C$ remains. If the deleted occurrence is the occurrence of $C$ used by identity, then the adjacent retained occurrence has the same formula and is also $C$. Thus the contracted sequent still has the form required by contextual identity. [/guided] [/step] [step:Push each operation through one logical inference] Let $R$ be the last inference in a derivation tree $\mathcal{D}$, and suppose the immediate premise derivations of $R$ have already been transformed. The last rule $R$ is one of the primitive logical rules for $\top$, $\bot$, $\land$, $\lor$, $\to$, $\forall$, or $\exists$. Apply the chosen context operation uniformly to every antecedent list in the displayed instance of $R$. By the uniform list-context reindexing hypothesis in the theorem statement, the resulting display is again an allowed instance of the same logical rule. The transformed immediate premise derivations prove exactly the transformed premises of this new rule instance. Reapplying that rule instance gives the transformed conclusion. For the quantifier rules, the formula occurrence inserted, exchanged, or contracted lies in an antecedent list. The bound variable and eigenvariable side conditions in the original rule instance are unchanged because the succedent formula, the quantified formula, and the chosen eigenvariable are not altered by the list-context operation. Hence the same eigenvariable condition remains valid after the transformation. [/step] [step:Run induction on the height of the source derivation] We prove the following simultaneous assertion by induction on $h(\mathcal{D})$: for each of the three context operations defined above, applying that operation to the end sequent of $\mathcal{D}$ gives a derivable sequent. If $h(\mathcal{D})=0$, then $\mathcal{D}$ is a contextual identity leaf, and the transformed sequent is derivable by the previous step on identity leaves. Assume the assertion for all derivation trees of height less than $h(\mathcal{D})$, and suppose $h(\mathcal{D})>0$. Let $R$ be the last inference of $\mathcal{D}$. Each immediate premise derivation has smaller height than $\mathcal{D}$, so the induction hypothesis transforms each premise derivation under the chosen context operation. The previous step then pushes that same operation through the last logical inference $R$ and rebuilds a derivation of the transformed conclusion. Thus the assertion holds for height $h(\mathcal{D})$, and induction gives it for every finite derivation tree. [/step] [step:Read off weakening, exchange, and contraction admissibility] Take any derivation of $\Gamma,\Delta \Rightarrow S$. Applying the insertion transformer with inserted formula $B$ gives a derivation of $\Gamma,B,\Delta \Rightarrow S$. Therefore left weakening in the form of insertion anywhere in the antecedent is admissible. Take any derivation of $\Gamma,A,B,\Delta \Rightarrow S$. Applying the adjacent exchange transformer gives a derivation of $\Gamma,B,A,\Delta \Rightarrow S$. Therefore adjacent left exchange is admissible. Take any derivation of $\Gamma,A,A,\Delta \Rightarrow S$. Applying the adjacent contraction transformer gives a derivation of $\Gamma,A,\Delta \Rightarrow S$. Therefore adjacent left contraction is admissible. These are exactly the three structural operations claimed in the theorem, so the proof is complete. [/step]