×

Upper estimates for lengthening the derivations in the case of the elimination of cuts. (Russian. English summary) Zbl 0562.03027

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

MSC:

03F05 Cut-elimination and normal-form theorems
03F20 Complexity of proofs
PDFBibTeX XMLCite
Full Text: EuDML