Ограниченный фрагмент исчисления Ламбека с операциями итерации и пересечения

Исчисление Ламбека (вариант интуиционистской линейной логики, изначально введённый для целей математической лингвистики) допускает естественные интерпретации на алгебре формальных языков ($\mathrm{L}$-модели) и на алгебре бинарных отношений — подмножеств некоторого фиксированного транзитивного отношения ($\mathrm{R}$-модели). Относительно обоих классов моделей имеют место теоремы о полноте (Андрека и Микулаш [J. Logic Lang. Inf., 3, No. 1 (1994), 1—37]; Пентус [Ann. Pure Appl. Logic, 75, Nos. 1/2 (1995), 179—213; Фундамент. и прикл. матем., 5, № 1 (1999), 193—219]). Операциями исчисления Ламбека являются умножение и два деления, левое и правое. Рассматривается расширение исчисления Ламбека операциями пересечения и итерации (звёздочка Клини). Доказывается, что это расширение неполно как относительно $\mathrm{L}$-моделей, так и относительно $\mathrm{R}$-моделей. Вводится ограниченный фрагмент, в котором итерация разрешена только в знаменателях делений, для него же доказывается полнота относительно $\mathrm{R}$-моделей. Полнота относительно $\mathrm{L}$-моделей доказывается для подсистемы без операции умножения. Оба результата являются теоремами о полноте в сильном смысле, т. е. устанавливают эквивалентность выводимости из множеств гипотез (которые могут быть конечными либо бесконечными) с одной стороны и семантического следования из множеств гипотез на данном классе моделей с другой. Также доказывается $\Pi_1^0$-полнота алгоритмической проблемы выводимости в рассматриваемом ограниченном фрагменте.