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

Обычное исчисление Ламбека задаёт атомарную теорию частично упорядоченных полугрупп с операциями левого и правого деления, а исчисление Ламбека с единицей — атомарную теорию частично упорядоченных моноидов с делениями. Обогащение сигнатуры операцией итерации даёт понятие алгебры Клини с делениями. Естественный пример такой алгебры - множество формальных языков, на котором заданы операции умножения, левого и правого делений и итерации Клини. В случае исчисления Ламбека без единицы рассматриваются языки без пустого слова, а вместо итерации Клини - положительная итерация.
В докладе будет представлена аксиоматизация исчисления Ламбека с итерацией, как с единицей, так и без неё, в виде секвенциальных (генценовских) исчислений. При этом используется правило вывода с бесконечным числом посылок ("омега-правило"). Для исчисления с положительной итерацией (без единицы) доказана $\Pi_1$-полнота проблемы выводимости. В частности, отсюда следует, что множество теорем этого исчисления не является рекурсивно перечислимым.
Аналогичный вопрос для исчисления Ламбека с единицей и итерацией Клини остаётся открытым.