Proof complexity of substructural logics

In this paper, we investigate the proof complexity of a wide range of substructural systems. For any proof system P at least as strong as Full Lambek calculus, FL, and polynomially simulated by the extended Frege system for some superintuitionistic logic of infinite branching, we present an exponential lower bound on the proof lengths. More precisely, we will provide a sequence of P-provable formulas {A_n}_n=1^∞ such that the length of the shortest 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 FL and any superintuitionistic logic of infinite branching. As an example, Hilbert-style proof systems for any finitely axiomatizable extension of FL that are weaker than the intuitionistic logic, in particular the usual Hilbert-style proof systems for the logics FL_S for the set of structural rules S⊆{e,i,o,c}, fall in this category. We will also prove a similar result for the proof systems and logics extending Visser's basic propositional calculus BPC and its logic 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 CFL_ew.