[Proof Complexity] New preprint

[Raheleh Jalali]

Dear Colleagues,

A new preprint is available at

http://arxiv.org/abs/2006.09705

Any comments and suggestions are more than welcome.

Best regards,
Raheleh Jalali.

Abstract:
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 infinite branching super-intuitionistic logic, 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}^{\infty}$ 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 infinite branching super-intuitionistic logic. 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}.