Разрешимость проблемы выводимости в LJ для класса формул, не содержащих отрицательных вхождений кванторов

Приводится разрешающий алгорифм для упомянутой в заглавии проблемы. Он основан на возможности указать для каждой формулы A, не содержащей отрицательных вхождений кванторов, такого числа N, что из выводимости $\to A$ в LJ следует существование такого вывода секвенции $\to A$ в LJ, в который входит не более чем $N$ переменных. Библ. 3 назв.