Structure of proofs and the complexity of cut elimination

The importance of the structure of cut-formulas with respect to proof length and proof depth has been studied in various occasions. It has been illustrated that a quantifier may be more powerful than a binary connective in cut-formulas with respect to the reduction (or increase) of proof length and proof depth, and a sequence of quantifiers of the same type (existential or universal) may be less powerful than a sequence of quantifiers of alternating types. This paper provides a refined view on cut-elimination through an analysis of the structure of proofs, brings new insight into the relation between cut-formulas and short proofs, and illustrates that a mixture of quantifiers and binary connectives could be important for achieving the maximal benefit of cut-formulas for obtaining short proofs.