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

S. V. Solov'ev

Zapiski Nauchnykh Seminarov POMI, Studies in constructive mathematics and mathematical logic. Part VIII, Tome 88 (1979), pp. 192-196

Résumé

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