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 show that the standard encoding
of the PHP as a monotone sequent admits quasipolynomial-size proofs
in this system. This result is a consequence of deriving the basic
properties of certain quasipolynomial-size monotone formulas
computing the boolean threshold functions. Since it is known that
the shortest proofs of the PHP in systems such as Resolution or
Bounded Depth Frege are exponentially long, it follows from our
result that these systems are exponentially separated from the
monotone Gentzen Calculus. We also consider the monotone sequent
(CLIQUE) expressing the {it clique}-{it coclique} principle
defined by Bonet, Pitassi and Raz (1997). 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, Cutting
Planes with polynomially bounded coefficients is also 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. Pudlak
