Abstract:
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$.