##
**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.

### MSC:

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.) |