Proof Complexity of Linear Logics

TL;DR

This paper investigates the proof-size complexity of classical propositional logic, revealing how structural rules like contraction and weakening significantly impact proof lengths and establishing exponential lower bounds for certain proof systems.

Contribution

It isolates the impact of structural rules on proof complexity, providing exponential lower bounds and demonstrating proof size differences across various linear logic systems.

Findings

Exponential proof-size lower bounds for LK without contraction.

Sub-exponential lower bounds for LK without weakening.

Existence of polynomial-size proofs in some systems that require exponential-size proofs in others.

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.