Cut normal forms and proof complexity (Q1302302)

Cut-elimination in first-order logic is known to have a non-elementary complexity. The authors investigate ``reduction classes'' \(K\) for cuts [cuts over formulas \(\notin K\) can be feasibly eliminated or replaced by cut-formulas in \(K]\) and for cut-elimination [if all cut formulas are in \(K\) then all cuts can be feasibly eliminated]. For \(K=\text{NNF}\) (negative normal form: no implication, and negations are applied only to atomic formulas) every cut is easily reduced to a formula in \(K\), and hence cut-elimination for \(K\) is not feasible. For \(K=\) Prenex Normal Forms there is a quadratic transformation of a proof with arbitrary cut-formulas into a proof with cut-formulas in \(K\) sending derivable formulas into \(K\). However, elimination of new cuts introduced in this way can be non-elementary. Monotone formulas are constructed by atoms including \(\perp\) by \(\forall,\exists,\&,\vee\). The authors prove that the elimination of non-monotone cuts has non-elementary complexity in the worst case. First, all monotone cuts are proved to be quickly (almost exponentially) eliminable from proofs of quasi-monotone formulas. Then it is noticed that Statman's sequence of equational sequents with no Kalmar-elementary bound for cut-elimination can be encoded by quasi-monotone formulas. The long proof of quick cut-elimination in the paper can be simplified using two observations. Statman's sequence is encoded by Horn formulas, and pruning transformations (underlying Harrop's theorem) allow drastically ``skolemize'' monotone formulas proved from universal Horn axioms.