Orevkov, V. P. Upper estimates for lengthening the derivations in the case of the elimination of cuts. (Russian. English summary) Zbl 0562.03027 Zap. Nauchn. Semin. Leningr. Otd. Mat. Inst. Steklova 137, 87-98 (1984). The purpose of this paper is to obtain such upper bounds for lengthening of proofs after cut-elimination, which depend on the number of sequences but not on the complexity of formulas. For commodity, the classical sequential calculus of predicates (KGL) and the constructive (intuitionistic) predicate calculus (IGL) are considered. Let D be a derivation-tree of a sequent S in the Gentzen calculus for KGL (or IGL), and define (inductively) \(2^ h_ i\) as follows: \(2^ h_ 0=h\); \(2^ h_{i+1}=2^{(2^ h_ i)}\). The main result of the paper is the existence of a cut-free proof D’ of S such that the height of D’ is less than \(2^ h_{\ell}\), where h is the height of D and \(\ell\) is the number of different sequents in D. Reviewer: N.Both Cited in 1 ReviewCited in 1 Document MSC: 03F05 Cut-elimination and normal-form theorems 03F20 Complexity of proofs Keywords:intuitionistic predicate calculus; bounds for lengthening of proofs after cut-elimination; classical sequential calculus of predicates; derivation- tree of a sequent; cut-free proof PDFBibTeX XMLCite \textit{V. P. Orevkov}, Zap. Nauchn. Semin. Leningr. Otd. Mat. Inst. Steklova 137, 87--98 (1984; Zbl 0562.03027) Full Text: EuDML