Upper bounds for lengthening of proofs after cut-elimination

V. P. Orevkov

Zapiski Nauchnykh Seminarov POMI, Computational complexity theory. Part II, Tome 137 (1984), pp. 87-98

Résumé

Define $2_i^n$ by $2_0^n=n$ and $2_{i+1}^n=2^{2_i^n}$. Let $\mathcal D$ be derivation tree of a sequent $S$ in the Gentzen-style calculus for the classical or intuitionistic first-order logic. The main result of the paper: There is a cut-free proof $\mathcal D'$ of $S$ such that the height of $\mathcal D'$ is less than $2^h_l$, where $h$ is the height of $\mathcal D$ and $l$ is the number of different sequents in $\mathcal D$.