[Proof Complexity] Prague seminar on Monday - Emil Jerabek
thapen
thapen at math.cas.cz
Sun May 14 00:03:50 CEST 2023
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 .
More information about the Proof-Complexity
mailing list