Characterising aspects of proof compression

Abstract

We consider deep inference proof formalisms, which are flexible enough to embed many widely used proof systems, and construe compression mechanisms `cut' and `dag' in a way that is independent of any particular proof system, but in a way that nonetheless has the same effect from the point of view of proof complexity. The main result of this work is an algebraic characterisation of situations when a tree-like system can polynomially simulate its dag-like counterpart. Other results include (1) that a particular deep inference rule, cocontraction, is equivalent to dagness, from the point of view of proof complexity; and (2) a generalisation of Krajicek's result that cut can simulate the behaviour of dagness in Frege systems.

NB: This article has had two previous names: Proof Compression Mechanisms and Deep Inference and Towards a General Treatment of Proof Compression Mechanisms.