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

Zap. Nauchn. Sem. LOMI, 1979 Volume 88, Pages 192–196 (Mi znsl3113)

This article is cited in 1 paper

A growth of length of $\mathrm L$-derivationtrans formed into natural deduction

S. V. Solov'ev


Abstract: Let $\varphi$ be a standard transformation [5] of Gentzen's $\mathrm L$-derivation $\alpha$ into natural deduction $\varphi(\alpha)$. We prove that $\operatorname{length}(\varphi(\alpha))\leq2^{2\cdot\operatorname{length}(\alpha)}$ where $\alpha$ is $(\&,\supset)$-Gentzen's intuitionistic $\mathrm L$-derivation.
This bound is almost optimal: an increasing sequence of $\mathrm L$-derivations $\alpha_i$ is constructed such that $\operatorname{length}(\varphi(\alpha_i))\leq2^{1/3\operatorname{length}(\alpha_i)}$.

UDC: 510.6


 English version:
Journal of Soviet Mathematics, 1982, 20:4, 2367–2369

Bibliographic databases:


© Steklov Math. Inst. of RAS, 2025