Preprint:
Samuel R. Buss, Leszek Aleksander Kołodziejczyk,
and Konrad Zdanowski
"Collapsing Modular Counting in Bounded Arithmetic
and Constant Depth Propositional Proofs"
Transactions of the American Mathematical Society 367 (2015) 7517-7563.
Download manuscript: PDF.
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 of bounded arithmetic 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 blowup 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.
Revised slides from related talks:
Collapsing Modular Counting in Bounded Arithmetic
and Constant Depth Propositional Proofs
Workshop on Limits of Theorem Proving (LiThPr)
Rome, Italy
September 26, 2012
Download Limits of Theorem Proving slides: PDF.