Proof Complexity of Substructural Logics
share
In this paper, we investigate the proof complexity of a wide range of substructural systems. For any proof system 𝐏 at least as strong as Full Lambek calculus, 𝐅𝐋, 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 𝐏-provable formulas {A_n}_n=1^∞ such that the length of the shortest 𝐏-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 𝖥𝖫 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 𝐁𝐏𝐂 and its logic 𝖡𝖯𝖢, 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 𝐂𝐅𝐋_𝐞𝐰.
READ FULL TEXT