[Proof Complexity] Preprint

[Anupam Das]

Dear all,

The following preprint (title and abstract below) may be interest to 
those on this list:

http://www.anupamdas.com/items/WeakMonProofsPHP/WeakMonProofsPHP.pdf

Any comments would be greatly appreciated.

Kind regards,
Anupam


The pigeonhole principle and related counting arguments in weak monotone 
systems

We construct quasipolynomial-size proofs of the propositional pigeonhole 
principle for the fragment of the sequent calculus with no cuts between 
ancestors of left and right negation, weakening and contraction rules.
The main construction of our argument, inspired by previous work on the 
monotone calculus by Atserias et al., provides formal proofs that 
permute the inputs of formulae computing threshold functions, 
essentially by implementing merge sort as a template.
Since it is non-trivial to eliminate the remaining weakening/contraction 
cuts efficiently, our arguments are implemented in deep inference where 
known normalization procedures exist, although this work is mostly 
self-contained. This also (partially) answers previous questions raised 
about the size of proofs of the pigeonhole principle in certain deep 
inference systems.