Proofs, computational complexity, and games

Abstract

This paper discusses the interplay between proof complexity, computational complexity, and combinatorial games. Classical proof theory typically concerns itself with the provability of sentences without considering the lengths of proofs. One of the basic results is that, for sufficiently rich theories, it is impossible to distinguish provable sentences from false sentences using an algorithm. In proof complexity, the lengths of proofs play a central role; hence the question is how difficult it is to distinguish propositions with polynomial-size proofs from false propositions, in particular, whether this is possible using an algorithm running in polynomial time. This problem is represented using the concept of canonical pairs of proof systems, which is closely connected with the concept of interpolation pairs of proof systems. Interpolation pairs allow us to connect proof systems to computational complexity problems and, for some proof systems, even to prove exponential lower bounds on the lengths of proofs. Our goal is to extend this approach to lower bounds to stronger systems, in particular, to constant-depth Frege proof systems. To this end, we have characterized the interpolation pairs of constant-depth Frege systems using certain combinatorial games. In this paper, we will define these games and explain their connection to some other concepts studied in proof complexity, specifically, the communication complexity versions of ᴛꜰɴᴘ classes. Our aim is to show that the three concepts studied in logic and computational complexity theory, playing combinatorial games, computing, and solving problems using communication between two players, are different facets of the same thing.