## Expander Construction
in VNC^{1}

#### 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 VNC^{1} corresponding to the ``NC^{1} 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 VNC^{1}. 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

- full version (January 2017)
- conference version in
*Innovations in Theoretical Computer Science (ITCS'17)*, 2017. - preliminary version in
*Electronic Colloquium on Computational Complexity*ECCC-TR16-144, 2016.