On the pigeonhole and related principles in deep inference and monotone systems
We construct quasipolynomial-size proofs of the
propositional pigeonhole principle in the deep inference system
KS, addressing an open problem raised in previous works and
matching the best known upper bound for the more general class
of monotone proofs.
We make significant use of monotone formulae computing
boolean threshold functions, an idea previously considered in
works of Atserias et al. The main construction, monotone
proofs witnessing the symmetry of such functions, involves an
implementation of merge-sort in the design of proofs in order to
tame the structural behaviour of atoms, and so the complexity
of normalization. Proof transformations from previous work on
atomic flows are then employed to yield appropriate KS proofs.
As further results we show that our constructions can be
applied to provide quasipolynomial-size KS proofs of the parity
principle and the generalized pigeonhole principle. These bounds
are inherited for the class of monotone proofs, and we are further
able to construct nO(log log n) -size monotone proofs of the weak
pigeonhole principle, thereby also improving the best known
bounds for monotone proofs.