Monotone proofs of the pigeon hole principle. (English) Zbl 0989.03065

Summary: We study the complexity of proving the Pigeon Hole Principle (PHP) 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 quasipolynomial-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 (CLIQUE) defined by M. Bonet, T. Pitassi and R. Raz [J. Symb. Log. 62, 708-728 (1997; Zbl 0889.03050)]. 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 quasipolynomial-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.


03F20 Complexity of proofs
68Q17 Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.)
68Q15 Complexity classes (hierarchies, relations among complexity classes, etc.)


Zbl 0889.03050
Full Text: DOI