Proof Complexity of Linear Logics

TL;DR

This work investigates the proof-size complexity of classical propositional logic by isolating the influence of structural rules in sequent calculi. By comparing contraction, weakening, and cut within substructural logics, it establishes exponential lower bounds for contraction-free systems, sub-exponential lower bounds for weakening-free systems, and exponential separations for cut-free versus cut-containing calculi, across frameworks like $ extbf{FL_e}$, $ extbf{FL_{ec}}$, $ extbf{ALL}$, $ extbf{RLL}$, and classical linear logics such as $ extbf{MALL}$, $ extbf{AMALL}$, and $ extbf{CLL}$. The methodology combines Chu's translation to transport bounds from intuitionistic to classical settings, a $ extbf{RLL}$–Vector Addition Systems connection to leverage reachability hardness, and feasible interpolation to derive explicit lower bounds, while also demonstrating exponential speed-ups when allowing cut. These results illuminate the precise role of structural rules in proof complexity and provide a blueprint for transferring lower bounds across logics. The findings have broad implications for understanding the inherent difficulty of proof systems and for guiding the design of more efficient proof calculi.

Abstract

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.