Abstract

We study the complexity of proving the Pigeon Hole Principle in a monotone variant of the Gentzen Calculus, also known as Geometric Logic. We prove a size-depth trade-off upper bound for monotone proofs of the standard encoding of the PHP as a monotone sequent. At one extreme of the trade-off we get quasipolynomia -size monotone proofs, and at the other extreme we get subexponential-size bounded-depth monotone proofs. This result is a consequence of deriving the basic properties of certain monotone formulas computing the Boolean threshold functions. We also consider the monotone sequent expressing the Clique-Coclique Principle defined by Bonet, Pitassi and Raz [9]. We show that monotone proofs for this sequent can be easily reduced to monotone proofs of the one-to-one and onto PHP, and so CLIQUE also has quasipolynomia -size monotone proofs. As a consequence of our results, Resolution, Cutting Planes with polynomially bounded coefficients, and Bounded-Depth Frege are exponentially separated from the monotone Gentzen Calculus. Finally, a simple simulation argument implies that these results extend to the Intuitionistic Gentzen Calculus. Our results partially answer some questions left open by P. Pudlák