Lower bounds for increasing complexity of derivations after cut elimination

We denote by C _k ^* the formula. In this paper for all k there is constructed a derivation of C _k ^* with cut, the number of sequents in which depends linearly on k. On the other hand, it is impossible to give an upper bound which is a Kalmar elementary function of k for the number of sequents in any derivation of the formula C _k ^* without cuts, or for the number of disjunctions in a refutation by the method of resolutions of systems of disjunctions corresponding to the negation of the formula C _k ^* . In particular, one can construct a derivation with cut of the formula C ₆ ^* , in which there is contained no more than 253 sequents, but in seeking a derivation of C ₆ ^* by the method of resolutions it is necessary to construct more than 10¹⁹²⁰⁰ disjunctions. With the help of Skolemization and taking out of quantifiers with respect to the formula C _k ^* there is constructed a formula v₀B _k ⁺ (v₀), which satisfies the following conditions: 1) one can construct a derivation with cuts of the formula v₀B _k ⁺ (v₀) in the constructive predicate calculus, the number of sequents in which depends linearly on k; 2) it is impossible to give an upper bound which is a Kalmar elementary function of k of the length of a term t such that the formula B _k ⁺ (t) is derivable.Translated from Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im. V. A. Steklova AN SSSR, Vol. 88, pp. 137–161, 1979.