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

TL;DR

This paper critiques Jerabek's claim of exponential lower bounds for implicational minimal logic, clarifying that their previous results on NP, coNP, and PSPACE equivalences remain valid and unrefuted.

Contribution

The paper clarifies misconceptions about Jerabek's approach, reaffirming the validity of earlier proof-theoretic results on complexity class equalities.

Findings

Jerabek's claim of exponential lower bounds is incorrect.

Previous proofs of NP = coNP = PSPACE remain valid.

The Basis example demonstrates the flaw in Jerabek's approach.

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\v{r}\'{a}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.