Рост длины секвенциального вывода при перестройке в натуральный

Рассматривается $(\&,\supset)$-фрагмент интуционистского исчисления высказываний. Показано, что при стандартной перестройке генценовского вывода $\alpha$ в натуральный вывод $\varphi(\alpha)$, длина $(\varphi(\alpha))\leq2^{2\cdot\text{длина}(\alpha)}$. Построена последовательность генценовских выводов возрастающей длины $\alpha'$, для которой длина $(\varphi(\alpha_i))\geq^{1/3\cdot\text{длина}(\alpha_i)}$ показывает, что полученная верхняя оценка является не слишком слабой. Библ. – 5 назв.