Expander Construction in VNC1

Sam Buss, Valentine Kabanets, Antonina Kolokolova, and Michal Koucký

Abstract

We give a combinatorial analysis, using edge expansion, of a variant of the iterative expander construction due to Reingold, Vadhan, and Wigderson [Annals of Mathematics, 2002], and show that this analysis can be formalized in the bounded-arithmetic system VNC1 corresponding to the ``NC1 reasoning''. As a corollary, we prove the assumption made by Jeřábek [Annals of Pure and Applied Logic, 2011] that a construction of certain bipartite expander graphs can be formalized in VNC1. This in turn implies that every proof in Gentzen's sequent calculus LK of a monotone sequent can be simulated in the monotone version of LK (MLK) with only polynomial blowup in proof size, strengthening the quasipolynomial simulation result of Atserias, Galesi, and Pudlák [Journal of Computer and System Sciences, 2002].

Versions