[Proof Complexity] paper (Expander Constructions in VNC-1)

Sam Buss sbuss at ucsd.edu
Thu Sep 15 23:21:25 CEST 2016

Dear Colleagues,

  A new paper, "Expander Constructions in VNC^1", by myself, Valentine
Kabanets, Antonina Kolokolova and Michal Koucky, is available from my web
page and also from ECCC,direct URL is

  Comments and other feedback are appreciated.

  Best regards, Sam Buss

We give a combinatorial analysis (using edge expansion) of a variant of the
iterative expander construction due to Reingold, Vadhan, and
Wigderson~\cite{RVW02}, 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\v{r}\'{a}bek \cite{Emil-aks} 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\'{a}k~\cite{AGP02}.

More information about the Proof-Complexity mailing list