Cut normal forms and proof complexity

Statman and Orevkov independently proved that cut-elimination is of nonelem entary complexity. Although their worst-case sequences are mathematically d ifferent the syntax of the corresponding cut formulas is of striking simila rity. This leads to the main question of this paper: to what extent is it p ossible to restrict the syntax of formulas and - at the same time - keep th eir power as cut formulas in a proof? We give a detailed analysis of this p roblem for negation normal form (NNF), prenex normal form (PNF) and monoton e formulas. We show that proof reduction to NNF is quadratic, while PNF beh aves differently: although there exists a quadratic transformation into a p roof in PNF too, additional cuts ape needed; the elimination of these cuts requires nonelementary expense in general. By restricting the logical opera tors to {boolean AND, boolean OR, For All, There Exists}, we obtain the typ e of monotone formulas. We prove that the elimination of monotone cuts can be of nonelementary complexity (here generalized disjunctions in the antece dents of sequents play a central role). On the other hand, we define a larg e class of problems (including all Horn theories) where cut-elimination of monotone cuts is only exponential and show that this bound is tight. This i mplies that the elimination of monotone cuts in equational theories is at m ost exponential. Particularly, there are no short proofs of Statman's seque nce with monotone cuts. (C) 1999 Elsevier Science B.V. All rights reserved.