Lower bounds for bounded depth Frege proofs via Pudlak-Buss games

Abstract

We present a simple proof of the bounded-depth Frege proof lower bounds of Pitassi et al. [1993] and Krajicek et al. [1995] for the pigeonhole principle. Our method uses the interpretation of proofs as two player games given by Pudlak and Buss. Our lower bound is conceptually simpler than previous ones, and relies on tools and intuition that are well known in the context of computational complexity. This makes the lower bound of Pitassi et al. [1993] and Krajicek et al. [1995] accessible to the general computational complexity audience. We hope this new view will open new directions for research in proof complexity.