Revision #2 Authors: Sam Buss, Valentine Kabanets, Antonina Kolokolova, Michal Koucky

Accepted on: 30th December 2016 21:36

Downloads: 246

Keywords:

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 Jerabek [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 Pudlak [Journal of Computer and System Sciences, 2002].

Corrected some typos and minor errors.

Revision #1 Authors: Sam Buss, Valentine Kabanets, Antonina Kolokolova, Michal Koucky

Accepted on: 13th October 2016 15:02

Downloads: 239

Keywords:

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 Jerabek [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 Pudlak [Journal of Computer and System Sciences, 2002].

Corrected some errors, and added some references (updating the related work).

TR16-144 Authors: Sam Buss, Valentine Kabanets, Antonina Kolokolova, Michal Koucky

Publication: 15th September 2016 23:02

Downloads: 464

Keywords:

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 Jerabek [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 Pudlak [Journal of Computer and System Sciences, 2002].