[Proof Complexity] Prague seminar on Monday - Emil Jerabek

[thapen]

Emil Jerabek will give a proof complexity talk in our logic seminar on
Monday 15th May, at 16:00 Prague time - see the announcement below.

It will be broadcast on zoom. To join use the link
https://cesnet.zoom.us/j/472648284?pwd=ZTlxeHhqWlltR1AzZC9CTHgzZ2tRZz09
Passcode: 017107 (if required)

-------------------------------------------------------------------------

Speaker: Emil Jerabek, Czech Academy of Sciences
Title: A simplified lower bound on intuitionistic implicational proofs

Abstract

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.

For more information see the seminar web page at
https://calendar.math.cas.cz/logic-seminar-actual .