Аннотация:
Сформулирован секвенциальный вариант интуиционистского исчисления предикатов с дополнительной одноместной логической связкой, интерпретируемой на древовидных моделях Крипке понятием запирания. Доказана полнота в классе моделей на деревьях высоты до $\omega^2$.