|
Zapiski Nauchnykh Seminarov LOMI, 1979, Volume 88, Pages 192–196
(Mi znsl3113)
|
|
|
|
This article is cited in 1 scientific paper (total 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)}$.
Citation:
S. V. Solov'ev, “A growth of length of $\mathrm L$-derivationtrans formed into natural deduction”, Studies in constructive mathematics and mathematical logic. Part VIII, Zap. Nauchn. Sem. LOMI, 88, "Nauka", Leningrad. Otdel., Leningrad, 1979, 192–196; J. Soviet Math., 20:4 (1982), 2367–2369
Linking options:
https://www.mathnet.ru/eng/znsl3113 https://www.mathnet.ru/eng/znsl/v88/p192
|
Statistics & downloads: |
Abstract page: | 139 | Full-text PDF : | 36 |
|