Remote Access Transactions of the American Mathematical Society
Green Open Access

Transactions of the American Mathematical Society

ISSN 1088-6850(online) ISSN 0002-9947(print)



Collapsing modular counting in bounded arithmetic and constant depth propositional proofs

Authors: Samuel R. Buss, Leszek Aleksander Kołodziejczyk and Konrad Zdanowski
Journal: Trans. Amer. Math. Soc. 367 (2015), 7517-7563
MSC (2010): Primary 03F20, 03F30, 03B05, 68Q15
Published electronically: February 26, 2015
MathSciNet review: 3391892
Full-text PDF

Abstract | References | Similar Articles | Additional Information

Abstract: Jeřábek introduced fragments of bounded arithmetic which are axiomatized with weak surjective pigeonhole principles and support a robust notion of approximate counting. We extend these fragments to accommodate modular counting quantifiers. These theories can formalize and prove the relativized versions of Toda's theorem on the collapse of the polynomial hierarchy with modular counting. We introduce a version of the Paris-Wilkie translation for converting formulas and proofs of bounded arithmetic with modular counting quantifiers into constant depth propositional logic with modular counting gates. We also define Paris-Wilkie translations to Nullstellensatz and polynomial calculus refutations. As an application, we prove that constant depth propositional proofs that use connectives AND, OR, and mod p gates, for $ p$ a prime, can be translated, with quasipolynomial increase in size, into propositional proofs containing only propositional formulas of depth three in which the top level is Boolean, the middle level consists of mod p gates, and the bottom level subformulas are small conjunctions. These results are improved to depth two by using refutations from the weak surjective pigeonhole principles.

References [Enhancements On Off] (What's this?)

  • [1] M. Ajtai, $ \Sigma ^{1}_{1}$-formulae on finite structures, Ann. Pure Appl. Logic 24 (1983), no. 1, 1-48. MR 706289 (85b:03048),
  • [2] M. Ajtai, The complexity of the pigeonhole principle, Proceedings of the 29-th Annual IEEE Symposium on Foundations of Computer Science, 1988, pp. 346-355, DOI 10.1109/SFCS.1988.21951.
  • [3] Eric Allender and Ulrich Hertrampf, Depth reduction for circuits of unbounded fan-in, Inform. and Comput. 112 (1994), no. 2, 217-238. MR 1280582 (95m:68050),
  • [4] Sanjeev Arora and Boaz Barak, Computational complexity, Cambridge University Press, Cambridge, 2009. A modern approach. MR 2500087 (2010i:68001)
  • [5] Toniann Pitassi, Paul Beame, and Russell Impagliazzo, Exponential lower bounds for the pigeonhole principle, Comput. Complexity 3 (1993), no. 2, 97-140. MR 1233662 (94f:03019),
  • [6] Paul Beame, Russell Impagliazzo, Jan Krajíček, Toniann Pitassi, and Pavel Pudlák, Lower bounds on Hilbert's Nullstellensatz and propositional proofs, Proc. London Math. Soc. (3) 73 (1996), no. 1, 1-26. MR 1387081 (97e:03072),
  • [7] Paul Beame and Søren Riis, More on the relative strength of counting principles, Proof complexity and feasible arithmetics (Rutgers, NJ, 1996) DIMACS Ser. Discrete Math. Theoret. Comput. Sci., vol. 39, Amer. Math. Soc., Providence, RI, 1998, pp. 13-35. MR 1486612 (99c:03082)
  • [8] Arnold Beckmann and Samuel R. Buss, Separation results for the size of constant-depth propositional proofs, Ann. Pure Appl. Logic 136 (2005), no. 1-2, 30-55. MR 2162846 (2006m:03090),
  • [9] Arnold Beckmann and Samuel R. Buss, Corrected upper bounds for free-cut elimination, Theoret. Comput. Sci. 412 (2011), no. 39, 5433-5445. MR 2857690,
  • [10] Arnold Beckmann and Samuel R. Buss, Improved witnessing and local improvement principles for second-order bounded arithmetic, to appear in ACM Transactions on Computational Logic, 2014.
  • [11] Richard Beigel and Jun Tarui, On $ {\rm ACC}$, Comput. Complexity 4 (1994), no. 4, 350-366. Special issue on circuit complexity (Barbados, 1992). MR 1313535 (96d:68060),
  • [12] Samuel R. Buss, Bounded arithmetic, Studies in Proof Theory. Lecture Notes, vol. 3, Bibliopolis, Naples, 1986. MR 880863 (89h:03104)
  • [13] Samuel R. Buss, Axiomatizations and conservation results for fragments of bounded arithmetic, Logic and computation (Pittsburgh, PA, 1987) Contemp. Math., vol. 106, Amer. Math. Soc., Providence, RI, 1990, pp. 57-84. MR 1057816 (91m:03059),
  • [14] Samuel R. Buss, Bounded arithmetic and propositional proof complexity, Logic of computation (Marktoberdorf, 1995) NATO Adv. Sci. Inst. Ser. F Comput. Systems Sci., vol. 157, Springer, Berlin, 1997, pp. 67-121. MR 1492461 (99b:03073)
  • [15] Samuel R. Buss, First-order proof theory of arithmetic, Handbook of proof theory, Stud. Logic Found. Math., vol. 137, North-Holland, Amsterdam, 1998, pp. 79-147. MR 1640326 (2000b:03208),
  • [16] Samuel Buss, R. Impagliazzo, J. Krajíček, P. Pudlák, A. A. Razborov, and J. Sgall, Proof complexity in algebraic systems and bounded depth Frege systems with modular counting, Comput. Complexity 6 (1996/97), no. 3, 256-298. MR 1486929 (99g:03060),
  • [17] Samuel R. Buss, Leszek Aleksander Kołodziejczyk, and Neil Thapen, Fragments of approximate counting, J. Symb. Log. 79 (2014), no. 2, 496-525. MR 3224978,
  • [18] Samuel R. Buss and Jan Krajíček, An application of Boolean complexity to separation problems in bounded arithmetic, Proc. London Math. Soc. (3) 69 (1994), no. 1, 1-21. MR 1272418 (96b:03074),
  • [19] Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo, Using the Groebner basis algorithm to find proofs of unsatisfiability, Computing (Philadelphia, PA, 1996) ACM, New York, 1996, pp. 174-183. MR 1427512,
  • [20] Stephen A. Cook, Feasibly constructive proofs and the propositional calculus (preliminary version), Seventh Annual ACM Symposium on Theory of Computing (Albuquerque, N.M., 1975), Assoc. Comput. Mach., New York, 1975, pp. 83-97. MR 0502226 (58 #19341)
  • [21] Nachum Dershowitz and Iddo Tzameret, Complexity of propositional proofs under a promise, ACM Trans. Comput. Log. 11 (2010), no. 3, Art. 18, 30. MR 2722828 (2012a:03157),
  • [22] Merrick Furst, James B. Saxe, and Michael Sipser, Parity, circuits, and the polynomial-time hierarchy, Math. Systems Theory 17 (1984), no. 1, 13-27. MR 738749 (86e:68048),
  • [23] Johan Håstad, Almost optimal lower bounds for small depth circuits, Advances in Computing Research, vol. 5, pp. 143-170, JAI Press, 1989.
  • [24] Emil Jeřábek, Dual weak pigeonhole principle, Boolean complexity, and derandomization, Ann. Pure Appl. Logic 129 (2004), no. 1-3, 1-37. MR 2078358 (2005e:03123),
  • [25] Emil Jeřábek, The strength of sharply bounded induction, MLQ Math. Log. Q. 52 (2006), no. 6, 613-624. MR 2282404 (2007k:03164),
  • [26] Emil Jeřábek, Approximate counting in bounded arithmetic, J. Symbolic Logic 72 (2007), no. 3, 959-993. MR 2354909 (2009b:03154),
  • [27] Emil Jeřábek, Approximate counting by hashing in bounded arithmetic, J. Symbolic Logic 74 (2009), no. 3, 829-860. MR 2548464 (2011i:03065),
  • [28] Jan Krajíček, Lower bounds to the size of constant-depth propositional proofs, J. Symbolic Logic 59 (1994), no. 1, 73-86. MR 1264964 (95k:03093),
  • [29] Jan Krajíček, Bounded arithmetic, propositional logic, and complexity theory, Encyclopedia of Mathematics and its Applications, vol. 60, Cambridge University Press, Cambridge, 1995. MR 1366417 (97c:03003)
  • [30] Jan Krajíček, Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic, J. Symbolic Logic 62 (1997), no. 2, 457-486. MR 1464108 (98k:03116),
  • [31] Alexis Maciel and Toniann Pitassi, Towards lower bounds for bounded-depth Frege proofs with modular connectives, Proof complexity and feasible arithmetics (Rutgers, NJ, 1996) DIMACS Ser. Discrete Math. Theoret. Comput. Sci., vol. 39, Amer. Math. Soc., Providence, RI, 1998, pp. 195-227. MR 1486622 (99c:03087)
  • [32] Alexis Maciel, Toniann Pitassi, and Alan R. Woods, A new proof of the weak pigeonhole principle, J. Comput. System Sci. 64 (2002), no. 4, 843-872. Special issue on STOC 2000 (Portland, OR). MR 1912305 (2003g:03096),
  • [33] J. B. Paris and A. J. Wilkie, $ \Delta _0$ sets and induction, Open Days in Model Theory and Set Theory (W. Guzicki, W. Marek, A. Pelc, and C. Rauszer, eds.), 1981, pp. 237-248.
  • [34] J. B. Paris and A. Wilkie, Counting problems in bounded arithmetic, Methods in mathematical logic (Caracas, 1983) Lecture Notes in Math., vol. 1130, Springer, Berlin, 1985, pp. 317-340. MR 799046 (87d:03167),
  • [35] J. B. Paris, A. J. Wilkie, and A. R. Woods, Provability of the pigeonhole principle and the existence of infinitely many primes, J. Symbolic Logic 53 (1988), no. 4, 1235-1244. MR 973114 (90d:03125),
  • [36] Chris Pollett, Structure and definability in general bounded arithmetic theories, Ann. Pure Appl. Logic 100 (1999), no. 1-3, 189-245. MR 1711988 (2000k:03132),
  • [37] A. A. Razborov, Lower bounds on the dimension of schemes of bounded depth in a complete basis containing the logical addition function, Mat. Zametki 41 (1987), no. 4, 598-607, 623 (Russian). MR 897705 (89h:03110)
  • [38] A. A. Razborov, On provably disjoint NP-pairs, Tech. Report RS-94-36, Basic Research in Computer Science Center, Aarhus, Denmark, November 1994,
  • [39] A. A. Razborov, Lower bounds for the polynomial calculus, Comput. Complexity 7 (1998), no. 4, 291-324. MR 1691494 (2000e:03158),
  • [40] Roman Smolensky, Algebraic methods in the theory of lower bounds for Boolean circuit complexity, Proceedings of the Nineteenth Annual ACM Symposium on the Theory of Computing, ACM Press, 1987, pp. 77-82, DOI 10.1145/28395.28404.
  • [41] Neil Thapen, A model-theoretic characterization of the weak pigeonhole principle, Ann. Pure Appl. Logic 118 (2002), no. 1-2, 175-195. MR 1934122 (2004e:03105),
  • [42] Neil Thapen, Higher complexity search problems for bounded arithmetic and a formalized no-gap theorem, Arch. Math. Logic 50 (2011), no. 7-8, 665-680. MR 2847538 (2012j:03139),
  • [43] Seinosuke Toda, PP is as hard as the polynomial-time hierarchy, SIAM J. Comput. 20 (1991), no. 5, 865-877. MR 1115655 (93a:68047),
  • [44] L. G. Valiant and V. V. Vazirani, NP is as easy as detecting unique solutions, Theoret. Comput. Sci. 47 (1986), no. 1, 85-93. MR 871466 (88i:68021),
  • [45] Andrew Chi-Chih Yao, On ACC and threshold circuits (St. Louis, MO, 1990), IEEE Comput. Soc. Press, Los Alamitos, CA, 1990, pp. 619-627. MR 1150721 (92k:68058),

Similar Articles

Retrieve articles in Transactions of the American Mathematical Society with MSC (2010): 03F20, 03F30, 03B05, 68Q15

Retrieve articles in all journals with MSC (2010): 03F20, 03F30, 03B05, 68Q15

Additional Information

Samuel R. Buss
Affiliation: Department of Mathematics, University of California, San Diego, La Jolla, California 92093-0112

Leszek Aleksander Kołodziejczyk
Affiliation: Institute of Mathematics, University of Warsaw, Banacha 2, 02-097 Warszawa, Poland

Konrad Zdanowski
Affiliation: Faculty of Mathematics and Natural Sciences, Cardinal Stefan Wyszyński University, Wóycickiego 1/3, 01-938 Warszawa, Poland

Received by editor(s): September 1, 2012
Received by editor(s) in revised form: June 21, 2013
Published electronically: February 26, 2015
Additional Notes: The first author was supported in part by NSF grants DMS-1101228 and CCR-1213151. In the preliminary stages of this work, the second and third authors were supported by grant no. N N201 382234 of the Polish Ministry of Science and Higher Education. Most of this work was carried out while the second author was visiting the University of California, San Diego, supported by the Polish Ministry of Science and Higher Education programme “Mobilność Plus” with additional support from a grant from the Simons Foundation (#208717 to Sam Buss).
Article copyright: © Copyright 2015 American Mathematical Society
The copyright for this article reverts to public domain 28 years after publication.

American Mathematical Society