Note: Pigeonhole principle in deep inference

I have written a short note on the proof complexity of the propositional 
pigeonhole principle for `cut-free' deep inference:

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

An outline of the material is given below this message.

Together with some other results, I am planning to expand this to a full 
article on the complexity of combinatorial principles in deep inference, 
using broadly the same techniques as presented here.

Unfortunately the note currently relies on much of the existing 
literature, hindering the accessibility of any article derived from it.

I would appreciate any feedback on this, especially regarding any 
possible simplifications or existing confusions.

Kind regards,
Anupam

A note on proofs of the pigeonhole principle in deep inference.

The propositional pigeonhole principle (PHP) is known to have 
polynomial-size proofs in systems with cut [Bus], and 
quasipolynomial-size ( n ^ (log^c n) ) proofs in deep inference systems 
that are cut-free but exhibit dag-like behaviour [Jer], [BGGP]. In the 
absence of this behaviour nothing is known, although it has recently 
been shown that the `functional' and `onto' variants have 
polynomial-size proofs [Das]. Here we consider the unrestricted version 
and give quasipolynomial-size proofs in such systems, matching the upper 
bounds when dag-like behaviour is permitted.

The main technique exploited is the observation that a restricted amount 
of dagness can be used in a proof, and then eliminated to give only a 
quasipolynomial blowup. Specifically, the observation is as follows: in 
any directed acyclic graph, if each node has out-degree quasipolynomial 
in the size of the graph and each path passes through at most 
polylogarithmically many nodes of out-degree greater than 1, then the 
naive tree-like expansion (by `folding out' the dags) has only 
quasipolynomial complexity. [Das]

Using this idea we employ the same approach as in [AGG] for providing 
monotone proofs of PHP, under a translation from monotone sequent proofs 
to cut-free deep inference proofs given in [Jer]. These proofs utilise 
negation-free `threshold formulae', formulae that assert that at least k 
out of n inputs are true; it is clear that their truth is preserved 
under permutation of the inputs. [AGG] gives a simple reduction of PHP 
to statements about certain permutations of variables in threshold 
formulae, and then the required task is to provide short proofs of this 
fact. The proofs given in [AGG] unfortunately do not satisfy the 
conditions in the above paragraph, and so the content of this note is 
mostly in providing alternative proofs that do satisfy the above conditions.

The specific permutation needed for PHP is switching of rows and columns 
of a square of variables or, equivalently, transposing a matrix. It is 
shown that this can be expressed as a composition of logarithmically 
`interleavings', themselves expressible by proofs satisfying the above 
conditions, whence the result follows. In ongoing work, we are 
attempting to extend the results to arbitrary permutations of variables 
in threshold formulae, via a generalisation of interleavings that form a 
basis of the symmetric group.


References

[AGG] Albert Atserias, Nicola Galesi, and Ricard Gavalda. Monotone 
proofs of the pigeon hole principle. 2000.
[Bus] Samuel R. Buss. Polynomial size proofs of the propositional 
pigeonhole principle. 1987.
[Das] Anupam Das. Complexity of deep inference via atomic flows. 2012.
[Jer] Emil Jerabek. Proof complexity of the cut-free calculus of 
structures. 2009.