On the pigeonhole and the modular counting principles over the bounded arithmetic $V^{0}$ (Theory and Applications of Proof and Computation)

Abstract

The theorem of Ajtai ([1], improved by [11] and [12]), which shows a superpolynomial lower bound for AC⁰-Frege proofs of the pigeonhole principle, was a significant breakthrough of proof complexity and has been inspiring many other important works considering the strengths of modular counting principles and the pigeonhole principle. In terms of bounded arithmetics, the theorem implies that the pigeonhole principle is independent from the bounded arithmetic V⁰. Along the stream of researches, [7] gave the following conjectures and showed some sufficient conditions to prove them: ・V⁰ ＋ UCP[l, d k] ∀ PHP[n+1 n].・For any prime number p other than 2, V⁰ ＋ oddtownk ∀ Count[p n].・For any integer p ≥ 2, V⁰ ＋ FIEk ∀ Count[p n]. Here, injPHP[n+1 n] is a formalization of the pigeonhole principle for injections, UCP[l, d k] is the uniform counting principle defined in [7], Count[p n] is the modular counting principle mod p, oddtownk is a formalization of odd town theorem, and FIEk is a formalization of Fisher's inequality. In this article, we give a summary of the work of [7], supplement both technical parts and motivations of it, and propose the future perspective.