Logic seminar

A simplified lower bound on intuitionistic implicational proofs

Unlike classical Frege systems, we know exponential lower bounds for some non-classical logics (modal, superintuitionistic, substructural), starting with seminal work of Hrubes (2007); they are all based on variants of the feasible disjunction property that play a similar role as monotone feasible interpolation for classical proof systems. This might suggest that disjunction is essential for these lower bounds, but Jerabek (2017) adapted them to the implicational fragment of intuitionistic logic. This results in a complex argument employing an implicational translation of intuitionistic logic on top of the proof of the lower bound proper, which in turn relies on monotone circuit lower bounds (Razborov, Alon-Boppana).

I will show how to prove the exponential lower bound directly for intuitionistic implicational logic without any translations, using a simple argument based on an efficient version of Kleene's slash. Apart from Frege, it applies directly to sequent calculus and (dag-like) natural deduction, obviating also the need for translation of these proof systems to Frege.

I will also mention a tangentially related problem about classical Frege systems.

One motivation for this work comes from presistent claims by Gordeev and Haeusler, who purport to show that all intuitionistic implicational tautologies have polynomial-size dag-like natural deduction proofs, implying NP = PSPACE. Their claims are false as they contradict the above-mentioned exponential lower bounds (and, in fact, also exponential lower bounds on constant-depth Frege), but for a non-specialist, understanding this requires tracking down multiple papers and some reading between the lines. Our argument consolidates all proof-theoretic components of the lower bound into one simple proof, depending only on the Alon-Boppana circuit lower bound.