Proof Complexity of Substructural Logics

TL;DR

This paper establishes exponential lower bounds on proof lengths for a broad class of substructural logics and proof systems, highlighting inherent complexity in their proof structures.

Contribution

It provides the first exponential lower bounds for proof lengths in various substructural systems and their extensions, extending known results to a wider range of logics.

Findings

Exponential lower bounds for proof lengths in systems at least as strong as Full Lambek calculus.

Lower bounds extend to proof-lines in Frege and extended Frege systems for certain logics.

Similar exponential bounds are proved for classical substructural proof systems extending Visser's calculus.

Abstract

In this paper, we investigate the proof complexity of a wide range of substructural systems. For any proof system $\mathbf{P}$ at least as strong as Full Lambek calculus, $\mathbf{FL}$, and polynomially simulated by the extended Frege system for some infinite branching super-intuitionistic logic, we present an exponential lower bound on the proof lengths. More precisely, we will provide a sequence of $\mathbf{P}$-provable formulas $\{A_n\}_{n=1}^{\infty}$ such that the length of the shortest $\mathbf{P}$-proof for $A_n$ is exponential in the length of $A_n$. The lower bound also extends to the number of proof-lines (proof-lengths) in any Frege system (extended Frege system) for a logic between $\mathsf{FL}$ and any infinite branching super-intuitionistic logic. We will also prove a similar result for the proof systems and logics extending Visser's basic propositional calculus $\mathbf{BPC}$ and its logic $\mathsf{BPC}$, respectively. Finally, in the classical substructural setting, we will establish an exponential lower bound on the number of proof-lines in any proof system polynomially simulated by the cut-free version of $\mathbf{CFL_{ew}}$.