Abstract: | 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
6
*
, in which there is contained no more than 253 sequents, but in seeking a derivation of C
6
*
by the method of resolutions it is necessary to construct more than 1019200 disjunctions. With the help of Skolemization and taking out of quantifiers with respect to the formula C
k
*
there is constructed a formula v0B
k
+
(v0), which satisfies the following conditions: 1) one can construct a derivation with cuts of the formula v0B
k
+
(v0) 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. |