Proof complexity of substructural logics (Q2032997)

The article is well written and organized, no typos where found. Three results are proved; the first one, is an exponential lower bound on the length of the proof of a sequence of hard \textbf{P}-tautologies \((\mathrm{Clique}_{n,k}\), and \(\mathrm{Color}_{n,m})\), namely a sequence of \textbf{P}-provable formulas \(\{A_n\}^\infty_{n=1}\), that is, the length of the shortest \textbf{P}-proof for \(A_n\) is exponential in \(|A_n|\), where \textbf{P} is a proof system as strong as full Lambek calculus (\textbf{FL}), and it is polynomially simulated by \textbf{eF} (extended Frege) for some superintuitionistic logic of \(\infty\)-branching, denoted by L-\textbf{EF}. The second result is a similar proof of the previous one but for a proof system and logic extending Visser's basic propositional calculus (\textbf{BPC}). And the third result is in the classical setting, again, an exponential lower bound on the number of proof line of any proof system polynomially simulated by \textbf{CLF}\(^{-}_{ew}\).