A note on proofs of the pigeonhole principle in deep inference


It is known that the functional and onto variants of the propositional pigeonhole principle have polynomial-size proofs in the weakest deep inference systems. The unrestricted variant has quasipolynomial-size proofs when dag-like behaviour is permitted. Here we match that upper bound in systems free of dag-ness, and indeed other compression mechanisms, utilising a similar strategy to that of Atserias, Galesi and Gavalda for the monotone sequent calculus.

NB: This note has been superseded by On the Pigeonhole and Related Principles in Deep Inference and Monotone Systems.