Expander Construction in VNC1

Authors Sam Buss, Valentine Kabanets, Antonina Kolokolova, Michal Koucky

Thumbnail PDF


  • Filesize: 0.64 MB
  • 26 pages

Document Identifiers

Author Details

Sam Buss
Valentine Kabanets
Antonina Kolokolova
Michal Koucky

Cite AsGet BibTex

Sam Buss, Valentine Kabanets, Antonina Kolokolova, and Michal Koucky. Expander Construction in VNC1. In 8th Innovations in Theoretical Computer Science Conference (ITCS 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 67, pp. 31:1-31:26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)


We give a combinatorial analysis (using edge expansion) of a variant of the iterative expander construction due to Reingold, Vadhan, and Wigderson (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 (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 (2002).
  • expander graphs
  • bounded arithmetic
  • alternating log time
  • sequent calculus
  • monotone propositional logic


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Miklós Ajtai, Janós Komlós, and Endre Szemerédi. An O(nlog n) sorting network. In Proceedings of the Fifteenth Annual ACM Symposium on Theory of Computing, pages 1-9. Association for Computing Machinery, 1983. Google Scholar
  2. Noga Alon and Fan R.K. Chung. Explicit construction of linear sized tolerant networks. Discrete Mathematics, 72:15-19, 1988. Google Scholar
  3. Noga Alon and Yuval Roichman. Random Cayley graphs and expanders. Random Structures and Algorithms, 5:271-284, 1994. Google Scholar
  4. Noga Alon, Oded Schwartz, and Asaf Shapira. An elementary construction of constant-degree expanders. Comb. Probab. Comput., 17(3):319-327, May 2008. URL: http://dx.doi.org/10.1017/S0963548307008851.
  5. Toshiyasu Arai. A bounded arithmetic AID for Frege systems. Annals of Pure and Applied Logic, 103:155-199, 2000. Google Scholar
  6. Albert Atserias, Nicola Galesi, and Ricard Gavaldá. Monotone proofs of the pigeon hole principle. Mathematical Logic Quarterly, 47(4):461-474, 2001. Google Scholar
  7. Albert Atserias, Nicola Galesi, and Pavel Pudlák. Monotone simulations of non-monotone proofs. Journal of Computer and System Sciences, 65(4):626-638, 2002. URL: http://dx.doi.org/10.1016/S0022-0000(02)00020-X.
  8. Marta Bílková. Monotone sequent calculus and resolution. Commentationes Mathematicae Universitatis Carolinae, 42:575-582, 2001. Google Scholar
  9. Sam Buss, Valentine Kabanets, Antonina Kolokolova, and Michal Koucký. Expander construction in VNC^1. Electronic Colloquium on Computational Complexity (ECCC), TR16-144, 2016. URL: http://eccc.hpi-web.de/report/2016/144/.
  10. Samuel R. Buss. Bounded Arithmetic. Bibliopolis, 1986. Revision of 1985 Princeton University Ph.D. thesis. Google Scholar
  11. Samuel R. Buss. Polynomial size proofs of the propositional pigeonhole principle. Journal of Symbolic Logic, 52:916-927, 1987. Google Scholar
  12. Samuel R. Buss, Leszek Aleksander Kołodziejczyk, and Konrad Zdanowski. Collapsing modular counting in bounded arithmetic and constant depth propositional proofs. Transactions of the AMS, 367:7517-7563, 2015. Google Scholar
  13. Peter Clote and Gaisi Takeuti. Bounded arithmetics for NC, ALOGTIME, L and NL. Annals of Pure and Applied Logic, 56:73-117, 1992. Google Scholar
  14. Stephen Cook and Phuong Nguyen. Logical Foundations of Proof Complexity. Cambridge University Press, New York, NY, USA, 1st edition, 2010. Google Scholar
  15. Stephen A. Cook. Feasibly constructive proofs and the propositional calculus. In Proceedings of the Seventh Annual ACM Symposium on Theory of Computing, pages 83-97, 1975. Google Scholar
  16. Stephen A. Cook and Tsuyoshi Morioka. Quantified propositional calculus and a second-order theory for NC¹. Archive for Mathematical Logic, 44:711-749, 2005. Google Scholar
  17. Irit Dinur. The PCP theorem by gap amplification. J. ACM, 54(3), June 2007. URL: http://dx.doi.org/10.1145/1236457.1236459.
  18. Ofer Gabber and Zvi Galil. Explicit construction of linear sized superconcentrators. Journal of Computer and System Sciences, 22:407-420, 1981. Google Scholar
  19. Shlomo Hoory, Nathan Linial, and Avi Wigderson. Expander graphs and their applications. Bulletin of the American Mathematical Society, 43(4):439-561, 2006. Google Scholar
  20. Emil Jeřábek. Approximate counting in bounded arithmetic. Journal of Symbolic Logic, 72(3):959-993, 2007. Google Scholar
  21. Emil Jeřábek. Approximate counting by hashing in bounded arithmetic. Journal of Symbolic Logic, 74(3):829-860, 2009. Google Scholar
  22. Emil Jeřábek. Substitution frege and extended frege proof systems in non-classical logics. Annals of Pure and Applied Logic, 159(1):1 - 48, 2009. URL: http://dx.doi.org/10.1016/j.apal.2008.10.005.
  23. Emil Jeřábek. On theories of bounded arithmetic for NC¹. Annals of Pure and Applied Logic, 162(4):322-340, 2011. Google Scholar
  24. Emil Jeřábek. A sorting network in bounded arithmetic. Annals of Pure and Applied Logic, 162(4):341-355, 2011. Google Scholar
  25. Alexander Lubotzky, Ralph Phillips, and Peter Sarnak. Ramanujan graphs. Combinatorica, 8(3):261-277, 1988. Google Scholar
  26. Alexis Maciel, Toniann Pitassi, and Alan R. Woods. A new proof of the weak pigeonhole principle. Journal of Computer and System Sciences, 64(4):843-872, 2002. Google Scholar
  27. Grigory Margulis. Explicit constructions of expanders. Problems of Information Transmission, pages 71-80, 1973. Google Scholar
  28. Milena Mihail. Conductance and convergence of Markov chains: A combinatorial treatment of expanders. In Proceedings of the Thirtieth Annual IEEE Symposium on Foundations of Computer Science, pages 526-531, 1989. Google Scholar
  29. Jeff B. Paris and Alex J. Wilkie. Δ₀ sets and induction. In W. Guzicki, W. Marek, A. Pelc, and C. Rauszer, editors, Open Days in Model Theory and Set Theory, pages 237-248, 1981. Google Scholar
  30. Jeff B. Paris, Alex J. Wilkie, and A. R. Woods. Provability of the pigeonhole principle and the existence of infinitely many primes. Journal of Symbolic Logic, 53:1235-1244, 1988. Google Scholar
  31. M. S. Paterson. Improved sorting networks with O(log N) depth. Algorithmica, 5(1-4):75-92, 1990. URL: http://dx.doi.org/10.1007/BF01840378.
  32. Jan Pich. Logical strength of complexity theory and a formalization of the PCP theorem in bounded arithmetic. Logical Methods in Computer Science, 11(2:8):1-38, 2015. Google Scholar
  33. Mark Pinsker. On the complexity of a concentrator. In Proceedings of the Seventh Annual Teletraffic Conference, pages 1-4, 1973. Google Scholar
  34. P. Pudlak. On the complexity of the propositional calculus. In S. Barry Cooper and John K.Editors Truss, editors, Sets and Proofs:, London Mathematical Society Lecture Note Series, page 197–218. Cambridge University Press, Jun 1999. Google Scholar
  35. Pavel Pudlák. Ramsey’s theorem in bounded arithmetic. In Computer Science Logic, Lecture Notes in Computer Science #553, pages 308-312. Springer-Verlag, 1992. Google Scholar
  36. Pavel Pudlák and Samuel R Buss. How to lie without being (easily) convicted and the lengths of proofs in propositional calculus. In International Workshop on Computer Science Logic, pages 151-162. Springer, 1994. Google Scholar
  37. Omer Reingold. Undirected connectivity in log-space. J. ACM, 55(4):17:1-17:24, September 2008. URL: http://dx.doi.org/10.1145/1391289.1391291.
  38. Omer Reingold, Salil Vadhan, and Avi Wigderson. Entropy waves, the zig-zag graph product, and new constant-degree expanders. Annals of Mathematics, 155(1):157-187, 2002. Google Scholar
  39. Eyal Rozenman and Salil P. Vadhan. Derandomized squaring of graphs. In Approximation, Randomization and Combinatorial Optimization, Algorithms and Techniques, 8th International Workshop on Approximation Algorithms for Combinatorial Optimization Problems, APPROX 2005 and 9th InternationalWorkshop on Randomization and Computation, RANDOM 2005, Berkeley, CA, USA, August 22-24, 2005, Proceedings, pages 436-447, 2005. Google Scholar
  40. Walter L. Ruzzo. On uniform circuit complexity. Journal of Computer and System Sciences, 22:365-383, 1981. Google Scholar
  41. Joel Seiferas. Sorting networks of logarithmic depth, further simplified. Algorithmica (New York), 53(3):374-384, 2009. URL: http://dx.doi.org/10.1007/s00453-007-9025-6.
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail