Harvard Logic Colloquium: Sam Buss (UCSD) "Bounded Arithmetic, Expanders, and Monotone Propositional Proofs"

This talk discusses a new combinatorial proof of the existence of expander graphs, which can be carried out in the bounded arithmetic theory VNC¹ corresponding to alternating linear time. As an application, we prove that the monotone propositional sequent calculus polynomially simulates the full propositional sequent calculus. Prior to this, only a quasipolynomial simulation was known. Joint work with Valentine Kabanets, Antonina Kolokolova, and Michal Koucky.