RUS  ENG
Full version
JOURNALS // Zapiski Nauchnykh Seminarov POMI // Archive

Zap. Nauchn. Sem. LOMI, 1984 Volume 137, Pages 87–98 (Mi znsl4788)

This article is cited in 1 paper

Upper bounds for lengthening of proofs after cut-elimination

V. P. Orevkov


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

UDC: 510.66



Bibliographic databases:


© Steklov Math. Inst. of RAS, 2025