Abstract
We give a combinatorial analysis (using edge expansion) of a variant of the iterative expander construction due to Reingold, Vadhan, and Wigderson [44], 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 Jerabek [28] 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 Pudlak [9]. (C) 2020 Elsevier B.V. All rights reserved.