Lower bounds for bounded depth Frege proofs via Pudlák-Buss games

Abstract

We present a simple proof of the bounded-depth Frege proof lower bounds of Pitassi et al. [1993] and Krajíček et al. [1995] for the pigeonhole principle. Our method uses the interpretation of proofs as two player games given by Pudlák 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 Krajíček et al. [1995] accessible to the general computational complexity audience. We hope this new view will open new directions for research in proof complexity.