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

[Sam Buss]

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
http://eccc.hpi-web.de/report/2016/144/.

  Comments and other feedback are appreciated.

  Best regards, Sam Buss

--
Abstract:
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}.