Upper bound on the lengthening of proofs by cut elimination

In this paper there are constructed sequential calculi KGL and IGL. The calculus KGI is a version of the classical predicate calculus, and IGL is a version of constructive calculus. KGL and IGL do not contain structural rules and there are no rules in them for which in some premise more than one lateral formula would be contained. A procedure for eliminating cuts from proofs in these calculi is described. It is shown that the height of a derivation obtained by this procedure exceeds 2 ^h, where h is the height of the original derivation, is the number of sequences in the original derivation,.Translated from Zapiski Nauchnykh Seminarov Leningradskogo Otdeleniya Matematicheskogo Instituta im. V. A. Steklova AN SSSR, Vol. 137, pp. 87–98, 1984.