Верхние оценки удлинения выводов при устранении сечений

В статье построены секвенциальные исчисления $KGL$ и $IGL$. Исчисление $KGL$ – вариант классического исчисления предикатов, $IGL$ – вариант конструктивного исчисления. $KGL$ и $IGL$ не содержат структурных правил и в них нет правил, у которых какая-нибудь посылка содержала бы более одной боковой формулы. Описана процедура устранения сечений из выводов в этих исчислениях. Показано, что высота вывода, полученного по этой процедуре, превосходит $2_l^h$, где $h$ – высота исходного вывода, $l$ – число секвенций в исходном выводе, $2_0^n=n$, $2_{i+1}^n=2^{2_i^n}$.