The Power of Structural Rules: Proof-Size Lower Bounds for Linear Logics

A longstanding challenge in proof complexity is to prove lower bounds on proof size in the classical sequent calculus. This talk sheds new light on this problem by isolating the contribution of individual structural rules. We show that the combined strength of contraction and weakening rules far exceeds that of any one of them in isolation. By restricting these rules one at a time, we obtain exponential or sub-exponential proof-size lower bounds for formulas that nevertheless admit short classical proofs. The results demonstrate that classical proof efficiency arises from the combination of structural rules.