Proving proof-size lower bounds for $\mathbf{LK}$, the sequent calculus for classical propositional logic, remains a major open problem in proof complexity. We shed new light on this challenge by isolating the power of structural rules, showing that their combination is extremely stronger than any single rule alone. We establish exponential (resp. sub-exponential) proof-size lower bounds for $\mathbf{LK}$ without contraction (resp. weakening) for formulas with short $\mathbf{LK}$-proofs. Concretely, we work with the Full Lambek calculus with exchange, $\mathbf{FL_e}$, and its contraction-extended variant, $\mathbf{FL_{ec}}$, substructural systems underlying linear logic. We construct families of $\mathbf{FL_e}$-provable (resp. $\mathbf{FL_{ec}}$-provable) formulas that require exponential-size (resp. sub-exponential-size) proofs in affine linear logic $\mathbf{ALL}$ (resp. relevant linear logic $\mathbf{RLL}$), but admit polynomial-size proofs once contraction (resp. weakening) is restored. This yields exponential lower bounds on proof-size of $\mathbf{FL_e}$-provable formulas in $\mathbf{ALL}$ and hence for $\mathbf{MALL}$, $\mathbf{AMALL}$, and full classical linear logic $\mathbf{CLL}$. Finally, we exhibit formulas with polynomial-size $\mathbf{FL_e}$-proofs that nevertheless require exponential-size proofs in cut-free $\mathbf{LK}$, establishing exponential speed-ups between various linear calculi and their cut-free counterparts.

翻译：证明经典命题逻辑的相继式演算系统 $\mathbf{LK}$ 的证明规模下界，仍然是证明复杂性领域的一个主要开放问题。我们通过分离结构规则的能力，揭示了这一挑战的新视角，表明这些规则的组合远比任何单一规则强大。我们针对具有短 $\mathbf{LK}$ 证明的公式，建立了不含收缩规则（对应地，不含弱化规则）的 $\mathbf{LK}$ 系统的指数级（对应地，亚指数级）证明规模下界。具体而言，我们研究带有交换性的完全兰贝克演算 $\mathbf{FL_e}$ 及其扩展了收缩规则的变体 $\mathbf{FL_{ec}}$，这些子结构系统是线性逻辑的基础。我们构造了 $\mathbf{FL_e}$ 可证明（对应地，$\mathbf{FL_{ec}}$ 可证明）的公式族，这些公式在仿射线性逻辑 $\mathbf{ALL}$（对应地，相关线性逻辑 $\mathbf{RLL}$）中需要指数规模（对应地，亚指数规模）的证明，但一旦恢复收缩规则（对应地，弱化规则），它们便拥有多项式规模的证明。这为 $\mathbf{FL_e}$ 可证明公式在 $\mathbf{ALL}$ 中的证明规模给出了指数下界，从而也适用于 $\mathbf{MALL}$、$\mathbf{AMALL}$ 以及完全经典线性逻辑 $\mathbf{CLL}$。最后，我们展示了一些具有多项式规模 $\mathbf{FL_e}$ 证明的公式，这些公式在无切割的 $\mathbf{LK}$ 系统中却需要指数规模的证明，从而确立了各种线性演算与其无切割对应系统之间的指数级加速。