Collapsing modular counting in bounded arithmetic and constant depth propositional proofs

Buss, Samuel; Kołodziejczyk, Leszek; Zdanowski, Konrad

doi:10.1090/S0002-9947-2015-06233-3

Collapsing modular counting in bounded arithmetic and constant depth propositional proofs
HTML articles powered by AMS MathViewer

by Samuel R. Buss, Leszek Aleksander Kołodziejczyk and Konrad Zdanowski PDF

Trans. Amer. Math. Soc. 367 (2015), 7517-7563 Request permission

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

M. Ajtai, $\Sigma ^{1}_{1}$-formulae on finite structures, Ann. Pure Appl. Logic 24 (1983), no. 1, 1–48. MR 706289, DOI 10.1016/0168-0072(83)90038-6
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.
Eric Allender and Ulrich Hertrampf, Depth reduction for circuits of unbounded fan-in, Inform. and Comput. 112 (1994), no. 2, 217–238. MR 1280582, DOI 10.1006/inco.1994.1057
Sanjeev Arora and Boaz Barak, Computational complexity, Cambridge University Press, Cambridge, 2009. A modern approach. MR 2500087, DOI 10.1017/CBO9780511804090
Toniann Pitassi, Paul Beame, and Russell Impagliazzo, Exponential lower bounds for the pigeonhole principle, Comput. Complexity 3 (1993), no. 2, 97–140. MR 1233662, DOI 10.1007/BF01200117
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, DOI 10.1112/plms/s3-73.1.1
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, DOI 10.1090/dimacs/039/02
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, DOI 10.1016/j.apal.2005.05.002
Arnold Beckmann and Samuel R. Buss, Corrected upper bounds for free-cut elimination, Theoret. Comput. Sci. 412 (2011), no. 39, 5433–5445. MR 2857690, DOI 10.1016/j.tcs.2011.05.053
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.
Richard Beigel and Jun Tarui, On $\textrm {ACC}$, Comput. Complexity 4 (1994), no. 4, 350–366. Special issue on circuit complexity (Barbados, 1992). MR 1313535, DOI 10.1007/BF01263423
Samuel R. Buss, Bounded arithmetic, Studies in Proof Theory. Lecture Notes, vol. 3, Bibliopolis, Naples, 1986. MR 880863
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, DOI 10.1090/conm/106/1057816
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
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, DOI 10.1016/S0049-237X(98)80017-7
S. 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, DOI 10.1007/BF01294258
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, DOI 10.1017/jsl.2013.37
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, DOI 10.1112/plms/s3-69.1.1
Matthew Clegg, Jeffery Edmonds, and Russell Impagliazzo, Using the Groebner basis algorithm to find proofs of unsatisfiability, Proceedings of the Twenty-eighth Annual ACM Symposium on the Theory of Computing (Philadelphia, PA, 1996) ACM, New York, 1996, pp. 174–183. MR 1427512, DOI 10.1145/237814.237860
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
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, DOI 10.1145/1740582.1740586
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, DOI 10.1007/BF01744431
Johan Håstad, Almost optimal lower bounds for small depth circuits, Advances in Computing Research, vol. 5, pp. 143–170, JAI Press, 1989.
Emil Jeřábek, Dual weak pigeonhole principle, Boolean complexity, and derandomization, Ann. Pure Appl. Logic 129 (2004), no. 1-3, 1–37. MR 2078358, DOI 10.1016/j.apal.2003.12.003
Emil Jeřábek, The strength of sharply bounded induction, MLQ Math. Log. Q. 52 (2006), no. 6, 613–624. MR 2282404, DOI 10.1002/malq.200610019
Emil Jeřábek, Approximate counting in bounded arithmetic, J. Symbolic Logic 72 (2007), no. 3, 959–993. MR 2354909, DOI 10.2178/jsl/1191333850
Emil Jeřábek, Approximate counting by hashing in bounded arithmetic, J. Symbolic Logic 74 (2009), no. 3, 829–860. MR 2548464, DOI 10.2178/jsl/1245158087
Jan Krajíček, Lower bounds to the size of constant-depth propositional proofs, J. Symbolic Logic 59 (1994), no. 1, 73–86. MR 1264964, DOI 10.2307/2275250
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, DOI 10.1017/CBO9780511529948
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, DOI 10.2307/2275541
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, DOI 10.1090/dimacs/039/12
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, DOI 10.1006/jcss.2002.1830
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.
J. 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, DOI 10.1007/BFb0075316
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, DOI 10.2307/2274618
Chris Pollett, Structure and definability in general bounded arithmetic theories, Ann. Pure Appl. Logic 100 (1999), no. 1-3, 189–245. MR 1711988, DOI 10.1016/S0168-0072(99)00008-1
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
A. A. Razborov, On provably disjoint NP-pairs, Tech. Report RS-94-36, Basic Research in Computer Science Center, Aarhus, Denmark, November 1994, http://www.brics.dk/index.html.
Alexander A. Razborov, Lower bounds for the polynomial calculus, Comput. Complexity 7 (1998), no. 4, 291–324. MR 1691494, DOI 10.1007/s000370050013
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.
Neil Thapen, A model-theoretic characterization of the weak pigeonhole principle, Ann. Pure Appl. Logic 118 (2002), no. 1-2, 175–195. MR 1934122, DOI 10.1016/S0168-0072(02)00038-6
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, DOI 10.1007/s00153-011-0240-0
Seinosuke Toda, PP is as hard as the polynomial-time hierarchy, SIAM J. Comput. 20 (1991), no. 5, 865–877. MR 1115655, DOI 10.1137/0220053
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, DOI 10.1016/0304-3975(86)90135-0
Andrew Chi-Chih Yao, On ACC and threshold circuits, 31st Annual Symposium on Foundations of Computer Science, Vol. I, II (St. Louis, MO, 1990) IEEE Comput. Soc. Press, Los Alamitos, CA, 1990, pp. 619–627. MR 1150721, DOI 10.1109/FSCS.1990.89583