A note on Jerabek's paper "A simplified lower bound for implicational logic"

TL;DR

This note comments on Je\v{r}\'{a}bek's approach that claimed to refute the equality NP = coNP = PSPACE by providing exponential lower bounds on the implicational minimal logic, which is wrong and misleading.

Abstract

In our previous papers we sketched proofs of the equality NP = coNP = PSPACE. These results have been obtained by proof theoretic tree-to-dag compressing techniques adapted to Prawitz's Natural Deduction (ND) for implicational minimal logic with references to Hudelmaier's cutfree sequent calculus. In this note we comment on Jeřábek's approach that claimed to refute our results by providing exponential lower bounds on the implicational minimal logic. This claim is wrong and misleading, which is briefly demonstrated by Basis example below.