Proof Complexity of Linear Logics

Abstract

Proving proof-size lower bounds for $\mathbf{LK}$, the sequent calculus for classical propositional logic, remains one of the major open problems in proof complexity. We shed new light on this challenge by isolating the power of structural rules and showing that their combination is dramatically stronger than any individual structural rule alone, even in the presence of the controlled structural rules provided by linear exponentials. It is easy to see that $\mathbf{LK}$ without the weakening rule is significantly weaker than $\mathbf{LK}$ with respect to proof complexity. It therefore remains to study the impact of eliminating contraction and cut. Working over the Full Lambek calculus with exchange, $\mathbf{FL_e}$, as a base system, we begin with the role of contraction. We construct families of $\mathbf{FL_e}$-provable formulas that require exponential-size proofs in affine linear logic $\mathbf{LLW}$, yet admit polynomial-size proofs once contraction is restored. This yields exponential proof-size lower bounds for $\mathbf{FL_e}$-provable formulas in $\mathbf{LLW}$, and consequently in $\mathbf{MALL}$, $\mathbf{MALL_w}$, and full classical linear logic $\mathbf{LL}$. We then investigate the role of cut. We exhibit sequents with polynomial-size $\mathbf{FL_e}$-proofs that nevertheless require exponential-size proofs in cut-free $\mathbf{LK}$. This shows that the cut rule alone provides an exponential speed-up over the combination of weakening and contraction. As a consequence, we obtain exponential separations between several linear calculi and their cut-free counterparts.