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