Overview
This research investigates proof-size lower bounds in the context of propositional logic, focusing on the role and impact of structural rules within various logical calculi. The study aims to clarify the contribution of individual structural rules and their combinations to proof complexity, particularly in relation to $\mathbf{LK}$, the sequent calculus for classical propositional logic.
Research Context
Determining proof-size lower bounds for $\mathbf{LK}$ is identified as a significant open problem in proof complexity. The study's approach involves isolating the power of structural rules to understand their effect. It notes that $\mathbf{LK}$ without the weakening rule is considerably weaker in proof complexity compared to $\mathbf{LK}$ with weakening. The research then proceeds to analyze the impact of eliminating contraction and cut.
Approach
The study operates within the framework of the Full Lambek calculus with exchange, $\mathbf{FL_e}$, as its foundational system. It first examines the role of contraction. To assess its impact, the researchers construct families of $\mathbf{FL_e}$-provable formulas. These formulas are then analyzed for their proof-size requirements in affine linear logic $\mathbf{LLW}$ both with and without the restoration of contraction.
Subsequently, the research investigates the role of the cut rule. This investigation involves exhibiting specific sequents that possess polynomial-size proofs in $\mathbf{FL_e}$. These sequents are then evaluated for their proof-size requirements in cut-free $\mathbf{LK}$.
Findings
- The combination of structural rules is characterized as dramatically stronger than any single structural rule when considered individually. This holds true even with the presence of controlled structural rules provided by linear exponentials.
- The weakening rule's absence significantly weakens $\mathbf{LK}$ in terms of proof complexity.
- Constructed families of $\mathbf{FL_e}$-provable formulas were found to necessitate exponential-size proofs within affine linear logic $\mathbf{LLW}$. However, these same formulas permit polynomial-size proofs once contraction is reintroduced.
- This observation yields exponential proof-size lower bounds for $\mathbf{FL_e}$-provable formulas in $\mathbf{LLW}$.
- Consequently, these exponential lower bounds extend to $\mathbf{MALL}$, $\mathbf{MALL_w}$, and full classical linear logic $\mathbf{LL}$.
- Sequents with polynomial-size $\mathbf{FL_e}$-proofs were identified. These specific sequents required exponential-size proofs in cut-free $\mathbf{LK}$.
- This indicates that the cut rule alone provides an exponential speed-up when compared to the combination of weakening and contraction.
- As a result of these findings, exponential separations were obtained between several linear calculi and their respective cut-free versions.